Expand description
The surface AST the four frontends produce and the checker consumes.
Its JSON form is the JavaScript runtime’s ({ "k": "binary", "op": "add", … }),
so the frontends of both runtimes can be compared node for node.
Structs§
- Guard
- The leading
if (n < 0n) throw …of a JavaScript parameter: a negative argument aborts with its message, the guards in their order. - SArray
Item - An element of an array literal, or with
spreadthe elements of an array. - SBinder
- SCase
- One case of a single-level match.
- SComparison
- SCtor
- SData
- SExpr
- A surface expression.
- SField
- SFn
- SMain
- SModule
- SParam
- SPattern
- A surface pattern.
- SProgram
- A parsed source program.
- SProof
- SProp
- A surface proposition.
- SRow
- One row of a multi-scrutinee surface match.
- SRule
- SSplit
- SSplit
Case - STag
Test - A JavaScript
x.$ === 'tag'(or!==) test: the tested value, the tag and the data type that has it. - STheorem
Enums§
- Binary
Op - Surface binary operators:
plusis JavaScript’s overloaded+. - Flavor
- Conversion semantics: exact, checked (aborts when out of range) or clamped.
- Rounding
- Division rounding a source operator asks for.
- SCase
Pattern - Patterns of a single-level match: one constructor, fields bound to names.
- SEffect
- SItem
- SNode
- SPattern
Node - SProp
Node - SStep
- A proof step:
tnames the tactic family. - Show
Style - How a value is printed: each source language’s own rendering.
- UnaryOp