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.