StrataDDM.Integration.Lean.ToExpr

source

@[implicit_reducible]

instance StrataDDM.QualifiedIdent.instToExpr :

Lean.ToExpr QualifiedIdent

Equations

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

source

@[implicit_reducible]

instance StrataDDM.SepFormat.instToExpr :

Lean.ToExpr SepFormat

Equations

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

source

def StrataDDM.astExprElab :

Lean.ParserDescr

Lift a DDM AST constructor that takes a polymorphic annotation value to the expression level with the correct number of arguments.

For example, astExpr! ArgF.ident ann returns a function that expects one Lean expression and returns another.

Equations

StrataDDM.astExprElab = Lean.ParserDescr.node `StrataDDM.astExprElab 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "astExpr!") (Lean.ParserDescr.const `ident))

Instances For

source

def StrataDDM.astExprElabImpl :

Lean.Elab.Term.TermElab

Equations

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

Instances For

source

def StrataDDM.astAnnExprElab :

Lean.ParserDescr

Equations

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

Instances For

source

def StrataDDM.astAnnExprElabImpl :

Lean.Elab.Term.TermElab

Equations

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

Instances For

source

@[implicit_reducible]

instance StrataDDM.SyntaxCatF.instToExpr {α : Type} [Lean.ToExpr α] :

Lean.ToExpr (SyntaxCatF α)

Equations

StrataDDM.SyntaxCatF.instToExpr = { toExpr := StrataDDM.SyntaxCatF.instToExpr._private_1, toTypeExpr := StrataDDM.SyntaxCatF.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.TypeExprF.instToExpr {α : Type} [Lean.ToExpr α] :

Lean.ToExpr (TypeExprF α)

Equations

StrataDDM.TypeExprF.instToExpr = { toExpr := StrataDDM.TypeExprF.instToExpr._private_1, toTypeExpr := StrataDDM.TypeExprF.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.ExprF.instToExpr {α : Type} [Lean.ToExpr α] :

Lean.ToExpr (ExprF α)

Equations

StrataDDM.ExprF.instToExpr = { toExpr := StrataDDM.ExprF.instToExpr._private_1, toTypeExpr := StrataDDM.ExprF.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.ArgF.instToExpr {α : Type} [Lean.ToExpr α] :

Lean.ToExpr (ArgF α)

Equations

StrataDDM.ArgF.instToExpr = { toExpr := StrataDDM.ArgF.instToExpr._private_1, toTypeExpr := StrataDDM.ArgF.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.OperationF.instToExpr {α : Type} [Lean.ToExpr α] :

Lean.ToExpr (OperationF α)

Equations

StrataDDM.OperationF.instToExpr = { toExpr := StrataDDM.OperationF.instToExpr._private_1, toTypeExpr := StrataDDM.OperationF.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.SourceRange.instToExpr :

Lean.ToExpr SourceRange

Equations

StrataDDM.SourceRange.instToExpr = { toExpr := fun (e : StrataDDM.SourceRange) => StrataDDM.SourceRange.instToExpr._private_1 e, toTypeExpr := StrataDDM.SourceRange.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.Ann.instToExpr {Base α : Type} [Lean.ToExpr Base] [Lean.ToExpr α] :

Lean.ToExpr (Ann Base α)

Equations

StrataDDM.Ann.instToExpr = { toExpr := fun (a : StrataDDM.Ann Base α) => StrataDDM.Ann.instToExpr._private_1 a, toTypeExpr := StrataDDM.Ann.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.PreType.instToExpr :

Lean.ToExpr PreType

Equations

StrataDDM.PreType.instToExpr = { toExpr := StrataDDM.PreType.instToExpr._private_1, toTypeExpr := StrataDDM.PreType.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.FunctionIterScope.instToExpr :

Lean.ToExpr FunctionIterScope

Equations

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

source

@[implicit_reducible]

instance StrataDDM.TypeRef.instToExpr :

Lean.ToExpr TypeRef

Equations

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

source

@[implicit_reducible]

instance StrataDDM.NamePatternPart.instToExpr :

Lean.ToExpr NamePatternPart

Equations

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

source

@[implicit_reducible]

instance StrataDDM.FunctionTemplate.instToExpr :

Lean.ToExpr FunctionTemplate

Equations

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

source

@[implicit_reducible]

instance StrataDDM.MetadataArg.instToExpr :

Lean.ToExpr MetadataArg

Equations

StrataDDM.MetadataArg.instToExpr = { toExpr := StrataDDM.MetadataArg.instToExpr._private_1, toTypeExpr := StrataDDM.MetadataArg.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.MetadataAttr.instToExpr :

Lean.ToExpr MetadataAttr

Equations

StrataDDM.MetadataAttr.instToExpr = { toExpr := fun (a : StrataDDM.MetadataAttr) => StrataDDM.MetadataAttr.instToExpr._private_1 a, toTypeExpr := StrataDDM.MetadataAttr.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.Metadata.instToExpr :

Lean.ToExpr Metadata

Equations

StrataDDM.Metadata.instToExpr = { toExpr := fun (m : StrataDDM.Metadata) => StrataDDM.Metadata.instToExpr._private_1 m, toTypeExpr := StrataDDM.Metadata.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.ArgDeclKind.instToExpr :

Lean.ToExpr ArgDeclKind

Equations

StrataDDM.ArgDeclKind.instToExpr = { toExpr := StrataDDM.ArgDeclKind.instToExpr._private_1, toTypeExpr := StrataDDM.ArgDeclKind.instToExpr._private_5 }

source

@[implicit_reducible]

instance StrataDDM.ArgDecl.instToExpr :

Lean.ToExpr ArgDecl

Equations

StrataDDM.ArgDecl.instToExpr = { toExpr := fun (b : StrataDDM.ArgDecl) => StrataDDM.ArgDecl.instToExpr._private_1 b, toTypeExpr := StrataDDM.ArgDecl.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.SyntaxDefAtom.instToExpr :

Lean.ToExpr SyntaxDefAtom

Equations

StrataDDM.SyntaxDefAtom.instToExpr = { toExpr := StrataDDM.SyntaxDefAtom.instToExpr._private_1, toTypeExpr := StrataDDM.SyntaxDefAtom.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.SyntaxDef.instToExpr :

Lean.ToExpr SyntaxDef

Equations

StrataDDM.SyntaxDef.instToExpr = { toExpr := StrataDDM.SyntaxDef.instToExpr._private_1, toTypeExpr := StrataDDM.SyntaxDef.instToExpr._private_5 }

source

@[implicit_reducible]

instance StrataDDM.SynCatDecl.instToExpr :

Lean.ToExpr SynCatDecl

Equations

StrataDDM.SynCatDecl.instToExpr = { toExpr := fun (d : StrataDDM.SynCatDecl) => StrataDDM.SynCatDecl.instToExpr._private_1 d, toTypeExpr := StrataDDM.SynCatDecl.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.DebruijnIndex.instToExpr {n : Nat} :

Lean.ToExpr (DebruijnIndex n)

Equations

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

source

def StrataDDM.DatatypeBindingSpec.toExpr {argDecls : ArgDecls} (b : DatatypeBindingSpec argDecls) (argDeclsExpr : Lean.Expr) :

Lean.Expr

Equations

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

Instances For

source

def StrataDDM.TvarBindingSpec.toExpr {argDecls : ArgDecls} (b : TvarBindingSpec argDecls) (argDeclsExpr : Lean.Expr) :

Lean.Expr

Equations

b.toExpr argDeclsExpr = Lean.mkApp2 (Lean.mkConst `StrataDDM.TvarBindingSpec.mk) argDeclsExpr (Lean.toExpr b.nameIndex)

Instances For

source

@[implicit_reducible]

instance StrataDDM.ArgDecls.instToExpr :

Lean.ToExpr ArgDecls

Equations

StrataDDM.ArgDecls.instToExpr = { toExpr := fun (a : StrataDDM.ArgDecls) => StrataDDM.ArgDecls.instToExpr._private_1 a, toTypeExpr := StrataDDM.ArgDecls.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.OpDecl.instToExpr :

Lean.ToExpr OpDecl

Equations

StrataDDM.OpDecl.instToExpr = { toExpr := fun (d : StrataDDM.OpDecl) => StrataDDM.OpDecl.instToExpr._private_1 d, toTypeExpr := StrataDDM.OpDecl.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.TypeDecl.instToExpr :

Lean.ToExpr TypeDecl

Equations

StrataDDM.TypeDecl.instToExpr = { toExpr := fun (d : StrataDDM.TypeDecl) => StrataDDM.TypeDecl.instToExpr._private_1 d, toTypeExpr := StrataDDM.TypeDecl.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.FunctionDecl.instToExpr :

Lean.ToExpr FunctionDecl

Equations

StrataDDM.FunctionDecl.instToExpr = { toExpr := fun (d : StrataDDM.FunctionDecl) => StrataDDM.FunctionDecl.instToExpr._private_1 d, toTypeExpr := StrataDDM.FunctionDecl.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.MetadataArgType.instToExpr :

Lean.ToExpr MetadataArgType

Equations

StrataDDM.MetadataArgType.instToExpr = { toExpr := StrataDDM.MetadataArgType.instToExpr._private_1, toTypeExpr := StrataDDM.MetadataArgType.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.MetadataArgDecl.instToExpr :

Lean.ToExpr MetadataArgDecl

Equations

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

source

@[implicit_reducible]

instance StrataDDM.MetadataDecl.instToExpr :

Lean.ToExpr MetadataDecl

Equations

StrataDDM.MetadataDecl.instToExpr = { toExpr := fun (d : StrataDDM.MetadataDecl) => StrataDDM.MetadataDecl.instToExpr._private_1 d, toTypeExpr := StrataDDM.MetadataDecl.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.Decl.Decl.instToExpr :

Lean.ToExpr Decl

Equations

StrataDDM.Decl.Decl.instToExpr = { toExpr := StrataDDM.Decl.Decl.instToExpr._private_1, toTypeExpr := StrataDDM.Decl.Decl.instToExpr._private_5 }

source

@[implicit_reducible]

instance StrataDDM.Dialect.instToExpr :

Lean.ToExpr Dialect

Equations

StrataDDM.Dialect.instToExpr = { toExpr := fun (d : StrataDDM.Dialect) => StrataDDM.Dialect.instToExpr._private_1 d, toTypeExpr := StrataDDM.Dialect.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.DialectMap.instToExpr :

Lean.ToExpr DialectMap

Equations

StrataDDM.DialectMap.instToExpr = { toExpr := fun (d : StrataDDM.DialectMap) => StrataDDM.DialectMap.instToExpr._private_1 d, toTypeExpr := StrataDDM.DialectMap.instToExpr._private_3 }

source

@[implicit_reducible]

instance StrataDDM.Program.instToExpr :

Lean.ToExpr Program

Equations

StrataDDM.Program.instToExpr = { toExpr := fun (ms : StrataDDM.Program) => StrataDDM.Program.instToExpr._private_1 ms, toTypeExpr := StrataDDM.Program.instToExpr._private_3 }