@[reducible, inline]
Equations
Instances For
Equations
- Lean.Meta.AC.instInhabitedPreContext = { default := { id := default, op := default, assoc := default, comm := default, idem := default } }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- op: Lean.Meta.AC.PreExpr → Lean.Meta.AC.PreExpr → Lean.Meta.AC.PreExpr
- var: Lean.Expr → Lean.Meta.AC.PreExpr
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- Lean.Meta.AC.toACExpr.toACExpr varMap (l.op r) = Lean.Data.AC.Expr.op (Lean.Meta.AC.toACExpr.toACExpr varMap l) (Lean.Meta.AC.toACExpr.toACExpr varMap r)
- Lean.Meta.AC.toACExpr.toACExpr varMap (Lean.Meta.AC.PreExpr.var x_1) = Lean.Data.AC.Expr.var (varMap x_1)
Instances For
def
Lean.Meta.AC.buildNormProof
(preContext : Lean.Meta.AC.PreContext)
(l : Lean.Expr)
(r : Lean.Expr)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Meta.AC.buildNormProof.mkContext
(preContext : Lean.Meta.AC.PreContext)
(α : Lean.Expr)
(u : Lean.Level)
(vars : Array Lean.Expr)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.AC.buildNormProof.convert (l.op r) = Lean.mkApp2 (Lean.mkConst `Lean.Data.AC.Expr.op) (Lean.Meta.AC.buildNormProof.convert l) (Lean.Meta.AC.buildNormProof.convert r)
- Lean.Meta.AC.buildNormProof.convert (Lean.Data.AC.Expr.var x_1) = Lean.mkApp (Lean.mkConst `Lean.Data.AC.Expr.var) (Lean.mkNatLit x_1)
Instances For
def
Lean.Meta.AC.buildNormProof.convertTarget
(preContext : Lean.Meta.AC.PreContext)
(vars : Array Lean.Expr)
:
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.AC.buildNormProof.convertTarget preContext vars (Lean.Data.AC.Expr.var x_1) = vars[x_1]!
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.AC.rewriteUnnormalizedRefl goal = do let __do_lift ← Lean.Meta.AC.rewriteUnnormalized goal __do_lift.refl
Instances For
Equations
- Lean.Meta.AC.acRflTactic x = do let goal ← Lean.Elab.Tactic.getMainGoal goal.withContext (liftM (Lean.Meta.AC.rewriteUnnormalizedRefl goal))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of the ac_nf
tactic when operating on the main goal.
Equations
- Lean.Meta.AC.acNfTargetTactic = Lean.Elab.Tactic.liftMetaTactic1 fun (goal : Lean.MVarId) => do let a ← Lean.Meta.AC.rewriteUnnormalized goal pure (some a)
Instances For
Implementation of the ac_nf
tactic when operating on a hypothesis.
Equations
- Lean.Meta.AC.acNfHypTactic fvarId = Lean.Elab.Tactic.liftMetaTactic1 fun (goal : Lean.MVarId) => Lean.Meta.AC.acNfHypMeta goal fvarId
Instances For
Equations
- One or more equations did not get rendered due to their size.