def
Lean.Grind.AC.Seq.denoteExpr
{M : Type → Type}
[Monad M]
[Meta.Grind.AC.MonadGetStruct M]
(s : Seq)
:
Equations
- One or more equations did not get rendered due to their size.
- (Lean.Grind.AC.Seq.var x).denoteExpr = do let __do_lift ← Lean.Meta.Grind.AC.getStruct pure __do_lift.vars[x]!
Instances For
def
Lean.Grind.AC.Expr.denoteExpr
{M : Type → Type}
[Monad M]
[Meta.Grind.AC.MonadGetStruct M]
(e : Expr)
:
Equations
- One or more equations did not get rendered due to their size.
- (Lean.Grind.AC.Expr.var x).denoteExpr = do let __do_lift ← Lean.Meta.Grind.AC.getStruct pure __do_lift.vars[x]!
Instances For
def
Lean.Meta.Grind.AC.EqCnstr.denoteExpr
{M : Type → Type}
[Monad M]
[MonadGetStruct M]
(c : EqCnstr)
:
M Expr
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Meta.Grind.AC.DiseqCnstr.denoteExpr
{M : Type → Type}
[Monad M]
[MonadGetStruct M]
(c : DiseqCnstr)
:
M Expr
Equations
- One or more equations did not get rendered due to their size.