inductive StrataDDM.Elab.BindingKind : Type

Information about the type or category of a bound variable.

• expr (tp : TypeExpr) : BindingKind

  Variable is an expression with the given type.

• type (ann : SourceRange) (params : List String) (value : Option TypeExpr) : BindingKind

  Variable is a type or parametric type.

  Type variables may be declared as synonyms for existing types. In this case, the value is a type expression over the parameters.

• cat (k : SyntaxCat) : BindingKind

  Variable belongs to the particular category below.

• tvar (ann : SourceRange) (name : String) : BindingKind

  Variable is a polymorphic type variable (for function type parameters). These are passed through to the dialect's typechecker for inference.

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedBindingKind : Inhabited BindingKind

Equations

• StrataDDM.Elab.instInhabitedBindingKind = { default := StrataDDM.Elab.instInhabitedBindingKind.default }

def StrataDDM.Elab.instInhabitedBindingKind.default : BindingKind

Equations

• StrataDDM.Elab.instInhabitedBindingKind.default = StrataDDM.Elab.BindingKind.expr default

@[implicit_reducible]

instance StrataDDM.Elab.instReprBindingKind : Repr BindingKind

Equations

• StrataDDM.Elab.instReprBindingKind = { reprPrec := StrataDDM.Elab.instReprBindingKind.repr }

def StrataDDM.Elab.instReprBindingKind.repr : BindingKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance StrataDDM.Elab.BindingKind.instCoeTypeExpr : Coe TypeExpr BindingKind

Equations

• StrataDDM.Elab.BindingKind.instCoeTypeExpr = { coe := fun (tp : StrataDDM.TypeExpr) => StrataDDM.Elab.BindingKind.expr tp }

def StrataDDM.Elab.BindingKind.ofCat (c : SyntaxCat) : BindingKind

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.BindingKind.categoryOf : BindingKind → SyntaxCat

Equations

• (StrataDDM.Elab.BindingKind.expr tp).categoryOf = StrataDDM.SyntaxCatF.atom (StrataDDM.TypeExprF.ann tp) { dialect := "Init", name := "Expr" }
• (StrataDDM.Elab.BindingKind.type loc params value).categoryOf = StrataDDM.SyntaxCatF.atom loc { dialect := "Init", name := "Type" }
• (StrataDDM.Elab.BindingKind.tvar loc name).categoryOf = StrataDDM.SyntaxCatF.atom loc { dialect := "Init", name := "Type" }
• (StrataDDM.Elab.BindingKind.cat c).categoryOf = c

@[implicit_reducible]

instance StrataDDM.Elab.BindingKind.instToStrataFormat : ToStrataFormat BindingKind

Equations

• StrataDDM.Elab.BindingKind.instToStrataFormat = { mformat := fun (bk : StrataDDM.Elab.BindingKind) => StrataDDM.Elab.BindingKind.instToStrataFormat._private_1 bk }

structure StrataDDM.Elab.Binding : Type

A single binder may declare multiple identifiers, but they all have the same type and metadata.

• ident : Var
• kind : BindingKind

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedBinding : Inhabited Binding

Equations

• StrataDDM.Elab.instInhabitedBinding = { default := StrataDDM.Elab.instInhabitedBinding.default }

def StrataDDM.Elab.instInhabitedBinding.default : Binding

Equations

• StrataDDM.Elab.instInhabitedBinding.default = { ident := default, kind := default }

def StrataDDM.Elab.instReprBinding.repr : Binding → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance StrataDDM.Elab.instReprBinding : Repr Binding

Equations

• StrataDDM.Elab.instReprBinding = { reprPrec := StrataDDM.Elab.instReprBinding.repr }

structure StrataDDM.Elab.Bindings : Type

A sequence of bindings.

Includes an additional map that maps the identifiers to the index of the binder for them.

• ofArray :: (
• toArray : Array Binding
• )

def StrataDDM.Elab.Bindings.ofList (l : List Binding) : Bindings

Equations

• StrataDDM.Elab.Bindings.ofList l = { toArray := l.toArray }

def StrataDDM.Elab.Bindings.isEmpty (b : Bindings) : Bool

Equations

• b.isEmpty = b.toArray.isEmpty

def StrataDDM.Elab.Bindings.size (b : Bindings) : Nat

Equations

• b.size = b.toArray.size

@[implicit_reducible]

instance StrataDDM.Elab.Bindings.instGetElemNatBindingLtSize : GetElem Bindings Nat Binding fun (bs : Bindings) (i : Nat) => i < bs.size

Equations

• StrataDDM.Elab.Bindings.instGetElemNatBindingLtSize = { getElem := fun (bindings : StrataDDM.Elab.Bindings) (idx : Nat) (p : idx < bindings.size) => bindings.toArray[idx] }

def StrataDDM.Elab.Bindings.empty : Bindings

Equations

• StrataDDM.Elab.Bindings.empty = { toArray := #[] }

@[implicit_reducible]

instance StrataDDM.Elab.Bindings.instEmptyCollection : EmptyCollection Bindings

Equations

• StrataDDM.Elab.Bindings.instEmptyCollection = { emptyCollection := StrataDDM.Elab.Bindings.empty }

@[implicit_reducible]

instance StrataDDM.Elab.Bindings.instInhabited : Inhabited Bindings

Equations

• StrataDDM.Elab.Bindings.instInhabited = { default := StrataDDM.Elab.Bindings.empty }

@[implicit_reducible]

instance StrataDDM.Elab.Bindings.instRepr : Repr Bindings

Equations

• StrataDDM.Elab.Bindings.instRepr = { reprPrec := fun (b : StrataDDM.Elab.Bindings) (prec : Nat) => Repr.addAppParen (Std.format "ofArray " ++ Std.format (reprArg b.toArray)) prec }

def StrataDDM.Elab.Bindings.push (bs : Bindings) (b : Binding) : Bindings

Equations

• bs.push b = { toArray := bs.toArray.push b }

def StrataDDM.Elab.Bindings.drop (bs : Bindings) (count : Nat) : Bindings

Remove the last i pushed bindings

Equations

• bs.drop count = if count = 0 then bs else { toArray := bs.toArray.take (bs.toArray.size - count) }

structure StrataDDM.Elab.TypingContext : Type

• globalContext : GlobalContext
• bindings : Bindings
• map : Std.HashMap Var (Array Nat)

@[implicit_reducible]

instance StrataDDM.Elab.instReprTypingContext : Repr TypingContext

Equations

• StrataDDM.Elab.instReprTypingContext = { reprPrec := StrataDDM.Elab.instReprTypingContext.repr }

def StrataDDM.Elab.instReprTypingContext.repr : TypingContext → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.TypingContext.empty (globalContext : GlobalContext) : TypingContext

Equations

• StrataDDM.Elab.TypingContext.empty globalContext = { globalContext := globalContext }

@[implicit_reducible]

instance StrataDDM.Elab.TypingContext.instInhabited : Inhabited TypingContext

Equations

• StrataDDM.Elab.TypingContext.instInhabited = { default := StrataDDM.Elab.TypingContext.empty ∅ }

def StrataDDM.Elab.TypingContext.push (tctx : TypingContext) (b : Binding) : TypingContext

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.TypingContext.drop (tctx : TypingContext) (count : Nat) : TypingContext

Remove the last count entries pushed to tctx.

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.TypingContext.ofBindings (bs : Bindings) : TypingContext

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.TypingContext.pushBindings (tctx : TypingContext) (b : Bindings) : TypingContext

Equations

• tctx.pushBindings b = Array.foldl StrataDDM.Elab.TypingContext.push tctx b.toArray

def StrataDDM.Elab.TypingContext.withGlobalContext (tctx : TypingContext) (gctx : GlobalContext) : TypingContext

Create a new TypingContext with a different GlobalContext but the same local bindings. Used for recursive datatype definitions where the datatype name needs to be added to the GlobalContext before parsing constructor field types.

Equations

• tctx.withGlobalContext gctx = { globalContext := gctx, bindings := tctx.bindings, map := tctx.map }

inductive StrataDDM.Elab.TypingContext.VarBinding : Type

This contains information about a bound or global variable.

• bvar (idx : Nat) (tpc : BindingKind) : VarBinding
• fvar (idx : FreeVarIndex) (tp : GlobalKind) : VarBinding

def StrataDDM.Elab.TypingContext.lookupVar (tctx : TypingContext) (var : String) : Option VarBinding

Equations

• One or more equations did not get rendered due to their size.

structure StrataDDM.Elab.ElabInfo : Type

Common information for each node in the Strata info tree.

• loc : SourceRange

  Source location information.

• inputCtx : TypingContext

  The typing context for node.

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedElabInfo : Inhabited ElabInfo

Equations

• StrataDDM.Elab.instInhabitedElabInfo = { default := StrataDDM.Elab.instInhabitedElabInfo.default }

def StrataDDM.Elab.instInhabitedElabInfo.default : ElabInfo

Equations

• StrataDDM.Elab.instInhabitedElabInfo.default = { loc := default, inputCtx := default }

@[implicit_reducible]

instance StrataDDM.Elab.instReprElabInfo : Repr ElabInfo

Equations

• StrataDDM.Elab.instReprElabInfo = { reprPrec := StrataDDM.Elab.instReprElabInfo.repr }

def StrataDDM.Elab.instReprElabInfo.repr : ElabInfo → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure StrataDDM.Elab.OperationInfoextends StrataDDM.Elab.ElabInfo : Type

• loc : SourceRange
• inputCtx : TypingContext
• op : Operation
• resultCtx : TypingContext

def StrataDDM.Elab.instInhabitedOperationInfo.default : OperationInfo

Equations

• StrataDDM.Elab.instInhabitedOperationInfo.default = { toElabInfo := default, op := default, resultCtx := default }

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedOperationInfo : Inhabited OperationInfo

Equations

• StrataDDM.Elab.instInhabitedOperationInfo = { default := StrataDDM.Elab.instInhabitedOperationInfo.default }

@[implicit_reducible]

instance StrataDDM.Elab.instReprOperationInfo : Repr OperationInfo

Equations

• StrataDDM.Elab.instReprOperationInfo = { reprPrec := StrataDDM.Elab.instReprOperationInfo.repr }

def StrataDDM.Elab.instReprOperationInfo.repr : OperationInfo → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure StrataDDM.Elab.CatInfoextends StrataDDM.Elab.ElabInfo : Type

• loc : SourceRange
• inputCtx : TypingContext
• cat : SyntaxCat

def StrataDDM.Elab.instInhabitedCatInfo.default : CatInfo

Equations

• StrataDDM.Elab.instInhabitedCatInfo.default = { toElabInfo := default, cat := default }

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedCatInfo : Inhabited CatInfo

Equations

• StrataDDM.Elab.instInhabitedCatInfo = { default := StrataDDM.Elab.instInhabitedCatInfo.default }

def StrataDDM.Elab.instReprCatInfo.repr : CatInfo → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance StrataDDM.Elab.instReprCatInfo : Repr CatInfo

Equations

• StrataDDM.Elab.instReprCatInfo = { reprPrec := StrataDDM.Elab.instReprCatInfo.repr }

structure StrataDDM.Elab.ExprInfoextends StrataDDM.Elab.ElabInfo : Type

• loc : SourceRange
• inputCtx : TypingContext
• expr : Expr

def StrataDDM.Elab.instInhabitedExprInfo.default : ExprInfo

Equations

• StrataDDM.Elab.instInhabitedExprInfo.default = { toElabInfo := default, expr := default }

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedExprInfo : Inhabited ExprInfo

Equations

• StrataDDM.Elab.instInhabitedExprInfo = { default := StrataDDM.Elab.instInhabitedExprInfo.default }

def StrataDDM.Elab.instReprExprInfo.repr : ExprInfo → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance StrataDDM.Elab.instReprExprInfo : Repr ExprInfo

Equations

• StrataDDM.Elab.instReprExprInfo = { reprPrec := StrataDDM.Elab.instReprExprInfo.repr }

structure StrataDDM.Elab.TypeInfoextends StrataDDM.Elab.ElabInfo : Type

• loc : SourceRange
• inputCtx : TypingContext
• typeExpr : TypeExpr
• isInferred : Bool

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedTypeInfo : Inhabited TypeInfo

Equations

• StrataDDM.Elab.instInhabitedTypeInfo = { default := StrataDDM.Elab.instInhabitedTypeInfo.default }

def StrataDDM.Elab.instInhabitedTypeInfo.default : TypeInfo

Equations

• StrataDDM.Elab.instInhabitedTypeInfo.default = { toElabInfo := default, typeExpr := default, isInferred := default }

def StrataDDM.Elab.instReprTypeInfo.repr : TypeInfo → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance StrataDDM.Elab.instReprTypeInfo : Repr TypeInfo

Equations

• StrataDDM.Elab.instReprTypeInfo = { reprPrec := StrataDDM.Elab.instReprTypeInfo.repr }

structure StrataDDM.Elab.ConstInfo (α : Type) extends StrataDDM.Elab.ElabInfo : Type

• loc : SourceRange
• inputCtx : TypingContext
• val : α

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedConstInfo {a✝ : Type} [Inhabited a✝] : Inhabited (ConstInfo a✝)

Equations

• StrataDDM.Elab.instInhabitedConstInfo = { default := StrataDDM.Elab.instInhabitedConstInfo.default }

def StrataDDM.Elab.instInhabitedConstInfo.default {a✝ : Type} [Inhabited a✝] : ConstInfo a✝

Equations

• StrataDDM.Elab.instInhabitedConstInfo.default = { toElabInfo := default, val := default }

def StrataDDM.Elab.instReprConstInfo.repr {α✝ : Type} [Repr α✝] : ConstInfo α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance StrataDDM.Elab.instReprConstInfo {α✝ : Type} [Repr α✝] : Repr (ConstInfo α✝)

Equations

• StrataDDM.Elab.instReprConstInfo = { reprPrec := StrataDDM.Elab.instReprConstInfo.repr }

@[reducible, inline]

abbrev StrataDDM.Elab.IdentInfo : Type

Equations

• StrataDDM.Elab.IdentInfo = StrataDDM.Elab.ConstInfo String

@[reducible, inline]

abbrev StrataDDM.Elab.NumInfo : Type

Equations

• StrataDDM.Elab.NumInfo = StrataDDM.Elab.ConstInfo Nat

@[reducible, inline]

abbrev StrataDDM.Elab.DecimalInfo : Type

Equations

• StrataDDM.Elab.DecimalInfo = StrataDDM.Elab.ConstInfo StrataDDM.Decimal

@[reducible, inline]

abbrev StrataDDM.Elab.StrlitInfo : Type

Equations

• StrataDDM.Elab.StrlitInfo = StrataDDM.Elab.ConstInfo String

structure StrataDDM.Elab.OptionInfoextends StrataDDM.Elab.ElabInfo : Type

• loc : SourceRange
• inputCtx : TypingContext

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedOptionInfo : Inhabited OptionInfo

Equations

• StrataDDM.Elab.instInhabitedOptionInfo = { default := StrataDDM.Elab.instInhabitedOptionInfo.default }

def StrataDDM.Elab.instInhabitedOptionInfo.default : OptionInfo

Equations

• StrataDDM.Elab.instInhabitedOptionInfo.default = { toElabInfo := default }

@[implicit_reducible]

instance StrataDDM.Elab.instReprOptionInfo : Repr OptionInfo

Equations

• StrataDDM.Elab.instReprOptionInfo = { reprPrec := StrataDDM.Elab.instReprOptionInfo.repr }

def StrataDDM.Elab.instReprOptionInfo.repr : OptionInfo → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure StrataDDM.Elab.SeqInfoextends StrataDDM.Elab.ElabInfo : Type

• loc : SourceRange
• inputCtx : TypingContext
• sep : SepFormat
• args : Array Arg
• resultCtx : TypingContext

def StrataDDM.Elab.instInhabitedSeqInfo.default : SeqInfo

Equations

• StrataDDM.Elab.instInhabitedSeqInfo.default = { toElabInfo := default, sep := default, args := default, resultCtx := default }

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedSeqInfo : Inhabited SeqInfo

Equations

• StrataDDM.Elab.instInhabitedSeqInfo = { default := StrataDDM.Elab.instInhabitedSeqInfo.default }

@[implicit_reducible]

instance StrataDDM.Elab.instReprSeqInfo : Repr SeqInfo

Equations

• StrataDDM.Elab.instReprSeqInfo = { reprPrec := StrataDDM.Elab.instReprSeqInfo.repr }

def StrataDDM.Elab.instReprSeqInfo.repr : SeqInfo → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive StrataDDM.Elab.Info : Type

• ofOperationInfo (info : OperationInfo) : Info
• ofCatInfo (info : CatInfo) : Info
• ofExprInfo (info : ExprInfo) : Info
• ofTypeInfo (info : TypeInfo) : Info
• ofIdentInfo (info : IdentInfo) : Info
• ofNumInfo (info : NumInfo) : Info
• ofDecimalInfo (info : DecimalInfo) : Info
• ofStrlitInfo (info : StrlitInfo) : Info
• ofBytesInfo (info : ConstInfo ByteArray) : Info
• ofOptionInfo (info : OptionInfo) : Info
• ofSeqInfo (info : SeqInfo) : Info

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedInfo : Inhabited Info

Equations

• StrataDDM.Elab.instInhabitedInfo = { default := StrataDDM.Elab.instInhabitedInfo.default }

def StrataDDM.Elab.instInhabitedInfo.default : Info

Equations

• StrataDDM.Elab.instInhabitedInfo.default = StrataDDM.Elab.Info.ofOperationInfo default

def StrataDDM.Elab.instReprInfo.repr : Info → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance StrataDDM.Elab.instReprInfo : Repr Info

Equations

• StrataDDM.Elab.instReprInfo = { reprPrec := StrataDDM.Elab.instReprInfo.repr }

def StrataDDM.Elab.Info.asOp! : Info → OperationInfo

Equations

• (StrataDDM.Elab.Info.ofOperationInfo info).asOp! = info
• x✝.asOp! = panicWithPosWithDecl "StrataDDM.Elab.Tree" "StrataDDM.Elab.Info.asOp!" 278 7 "Expected operation"

def StrataDDM.Elab.Info.asExpr! : Info → ExprInfo

Equations

• (StrataDDM.Elab.Info.ofExprInfo info).asExpr! = info
• x✝.asExpr! = panicWithPosWithDecl "StrataDDM.Elab.Tree" "StrataDDM.Elab.Info.asExpr!" 282 10 (toString "Expected expression but given " ++ toString (repr x✝))

def StrataDDM.Elab.Info.asType! : Info → TypeInfo

Equations

• (StrataDDM.Elab.Info.ofTypeInfo info).asType! = info
• x✝.asType! = panicWithPosWithDecl "StrataDDM.Elab.Tree" "StrataDDM.Elab.Info.asType!" 286 10 (toString "Expected type but given " ++ toString (repr x✝))

def StrataDDM.Elab.Info.asIdent! : Info → IdentInfo

Equations

• (StrataDDM.Elab.Info.ofIdentInfo info).asIdent! = info
• x✝.asIdent! = panicWithPosWithDecl "StrataDDM.Elab.Tree" "StrataDDM.Elab.Info.asIdent!" 290 7 "Expected identifier"

def StrataDDM.Elab.Info.elabInfo (info : Info) : ElabInfo

Equations

• (StrataDDM.Elab.Info.ofOperationInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofCatInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofExprInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofTypeInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofIdentInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofNumInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofDecimalInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofStrlitInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofBytesInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofOptionInfo a).elabInfo = a.toElabInfo
• (StrataDDM.Elab.Info.ofSeqInfo a).elabInfo = a.toElabInfo

def StrataDDM.Elab.Info.inputCtx (info : Info) : TypingContext

Equations

• info.inputCtx = info.elabInfo.inputCtx

def StrataDDM.Elab.Info.loc (info : Info) : SourceRange

Equations

• info.loc = info.elabInfo.loc

inductive StrataDDM.Elab.Tree : Type

• node (info : Info) (children : Array Tree) : Tree

def StrataDDM.Elab.instInhabitedTree.default : Tree

Equations

• StrataDDM.Elab.instInhabitedTree.default = StrataDDM.Elab.Tree.node default default

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedTree : Inhabited Tree

Equations

• StrataDDM.Elab.instInhabitedTree = { default := StrataDDM.Elab.instInhabitedTree.default }

@[implicit_reducible]

instance StrataDDM.Elab.instReprTree : Repr Tree

Equations

• StrataDDM.Elab.instReprTree = { reprPrec := StrataDDM.Elab.instReprTree.repr }

partial def StrataDDM.Elab.instReprTree.repr : Tree → Nat → Std.Format

def StrataDDM.Elab.Tree.info : Tree → Info

Equations

• (StrataDDM.Elab.Tree.node info children).info = info

def StrataDDM.Elab.Tree.children : Tree → Array Tree

Equations

• (StrataDDM.Elab.Tree.node info children).children = children

@[implicit_reducible]

instance StrataDDM.Elab.Tree.instGetElemNatLtSizeChildren : GetElem Tree Nat Tree fun (t : Tree) (i : Nat) => i < t.children.size

Equations

• StrataDDM.Elab.Tree.instGetElemNatLtSizeChildren = { getElem := fun (xs : StrataDDM.Elab.Tree) (i : Nat) (h : i < xs.children.size) => xs.children[i] }

@[simp]

theorem StrataDDM.Elab.Tree.node_getElem (info : Info) (c : Array Tree) (i : Nat) (p : i < (node info c).children.size) : (node info c)[i] = c[i]

def StrataDDM.Elab.Tree.arg : Tree → Arg

theorem StrataDDM.Elab.Tree.sizeOf_children (t : Tree) (i : Nat) (p : i < t.children.size) : sizeOf t[i] < sizeOf t

@[irreducible]

def StrataDDM.Elab.Tree.resultContext (t : Tree) : TypingContext

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.Tree.isSpecificOp (tree : Tree) (expected : QualifiedIdent) : Bool

Equations

• tree.isSpecificOp expected = match tree.info with | StrataDDM.Elab.Info.ofOperationInfo info => decide (info.op.name = expected) | x => false

def StrataDDM.Elab.Tree.asOption? (t : Tree) : Option (Option Tree)

Equations

• t.asOption? = match t.info with | StrataDDM.Elab.Info.ofOptionInfo info => some t.children[0]? | x => none

def StrataDDM.Elab.Tree.asCommaSepInfo? (t : Tree) : Option (Array Tree)

Equations

• t.asCommaSepInfo? = match t.info with | StrataDDM.Elab.Info.ofSeqInfo info => if (info.sep == StrataDDM.SepFormat.comma) = true then some t.children else none | x => none

def StrataDDM.Elab.Tree.asCommaSepInfo! (t : Tree) : Array Tree

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.Tree.optBindings! (optBindingsTree : Tree) : Array Tree

Retun array of bindings for a tree with category Option Bindings

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.Tree.asBindingType! (tree : Tree) : Tree

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.Tree.binding! (tree : Tree) : IdentInfo × Tree × Option Tree

Equations

• One or more equations did not get rendered due to their size.