def
Lean.MetavarContext.occursCheck
(mctx : Lean.MetavarContext)
(mvarId : Lean.MVarId)
(e : Lean.Expr)
:
Equations
- Lean.MetavarContext.occursCheck mctx mvarId e = (fun visitMVar visit => if (!Lean.Expr.hasExprMVar e) = true then true else match EStateM.run (visit e) ∅ with | EStateM.Result.ok x x_1 => true | EStateM.Result.error x x_1 => false) (Lean.MetavarContext.occursCheck.visitMVar mctx mvarId) (Lean.MetavarContext.occursCheck.visit mctx mvarId)
partial def
Lean.MetavarContext.occursCheck.visitMVar
(mctx : Lean.MetavarContext)
(mvarId : Lean.MVarId)
(mvarId' : Lean.MVarId)
:
partial def
Lean.MetavarContext.occursCheck.visit
(mctx : Lean.MetavarContext)
(mvarId : Lean.MVarId)
(e : Lean.Expr)
: