@[reducible, inline]

abbrev Core.ExpressionMetadata : Type

Equations

• Core.ExpressionMetadata = Unit

@[reducible, inline]

abbrev Core.Expression : Imperative.PureExpr

Equations

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

instance Core.instHasVarsPureExpressionExpr : Imperative.HasVarsPure Expression Expression.Expr

Equations

• Core.instHasVarsPureExpressionExpr = { getVars := Lambda.LExpr.LExpr.getVars }

instance Core.instInhabitedExprExpression : Inhabited Expression.Expr

Equations

• Core.instInhabitedExprExpression = { default := Lambda.LExpr.intConst () 0 }