pub struct TopLet {
pub let_kw: KwLet,
pub stage: Option<TopStage>,
pub name: BindName,
pub ascription: Option<RecAscription>,
pub leading_bar: Option<BarTok>,
pub params: Vec<Param>,
pub eq: DefEqTok,
pub value: Expr,
}Expand description
A top-level non-recursive binding: let name param* = expr. params is
Vec<ast::PatBot> (not merely Vec<VarTok>) — nxnonrecdec’s argpart
is patbot* upstream too, matching ast::RecBinding’s field of the same
name. Elaborated by the same rec_clause_value helper RecBinding uses
(elaborate.rs), with no multi-clause extra.
Fields§
§let_kw: KwLet§stage: Option<TopStage>The stage this ONE binding is written at, when it is not the default
(see TopStage). 0.0.6 source never sets it — 0.0.6 declares a
stage per FILE, with a @stage: header — so it parses as None for
every 0.0.6 program; it exists because SATySFi 0.1 declares the
stage per BINDING (val ~x = e, parser_v1.mly:417-421) and
v1/lower.rs lowers 0.1 binds into this very node. Carrying the
stage ON the binding (rather than in a side table keyed by prelude
index, which is how the 0.0.6 @stage: header reaches
elaborate.rs) is what lets it survive the loader’s prelude merge,
module nesting and cross-version splicing unharmed: an index-keyed
map cannot name a binding inside a module … = struct … end, and
every 0.1 val is inside one.
name: BindName§ascription: Option<RecAscription>Optional : ty type ascription (let f : ty x = e, let x : ty = e),
upstream’s patbotwithann — parse-and-ignore, exactly like
ast::RecBinding::ascription (this untyped elaborator has nothing to
check it against). Sits before params, matching patbotwithann argpart.
leading_bar: Option<BarTok>The | upstream’s nonrecdecargpart allows between the name (or its
ascription) and the argument list — let f : τ | x = e and
let f | x = e, parser.mly:610-614. Unlike let-rec’s, a non-rec
| introduces NO further clauses (nonrecdecargpart has no
nxrecdecpar tail): it is purely a separator, so nothing downstream
reads this field — it exists to make verbatim upstream source parse,
exactly like ast::RecBinding::leading_bar.
Real source writes it: azmath’s util.satyh opens with
let math-in-math : math-class -> (context -> math) -> math
| mcls embedf = .., and without this the whole file failed at its
first binding — the package’s ONLY blocker, in both the 0.0.6 and
the cross-version arm.
params: Vec<Param>§eq: DefEqTok§value: ExprTrait Implementations§
Source§impl<__SyanMacro_Atom> Parse<__SyanMacro_Atom> for TopLetwhere
__SyanMacro_Atom: Spanned + Clone,
KwLet: Parse<__SyanMacro_Atom>,
Option<TopStage>: Parse<__SyanMacro_Atom>,
BindName: Parse<__SyanMacro_Atom>,
Option<RecAscription>: Parse<__SyanMacro_Atom>,
Option<BarTok>: Parse<__SyanMacro_Atom>,
Vec<Param>: Parse<__SyanMacro_Atom>,
DefEqTok: Parse<__SyanMacro_Atom>,
Expr: Parse<__SyanMacro_Atom>,
impl<__SyanMacro_Atom> Parse<__SyanMacro_Atom> for TopLetwhere
__SyanMacro_Atom: Spanned + Clone,
KwLet: Parse<__SyanMacro_Atom>,
Option<TopStage>: Parse<__SyanMacro_Atom>,
BindName: Parse<__SyanMacro_Atom>,
Option<RecAscription>: Parse<__SyanMacro_Atom>,
Option<BarTok>: Parse<__SyanMacro_Atom>,
Vec<Param>: Parse<__SyanMacro_Atom>,
DefEqTok: Parse<__SyanMacro_Atom>,
Expr: Parse<__SyanMacro_Atom>,
Source§type Error = ParseError<<__SyanMacro_Atom as Spanned>::Span>
type Error = ParseError<<__SyanMacro_Atom as Spanned>::Span>
<FieldTy as Parse<Atom>>::Error: Into<…> predicate re-creates a projection cycle on a
recursive field (E0275), which decycle’s bound-peeling does not break.