def Auto.Meta.isDefEqD (t s : Lean.Expr) : Lean.MetaM Bool

Equations

• Auto.Meta.isDefEqD t s = Lean.Meta.withDefault (Lean.Meta.isDefEq t s)

def Auto.Meta.whnfNondependentForall (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

partial def Auto.Meta.normalizeNondependentForall (e : Lean.Expr) : Lean.MetaM Lean.Expr

def Auto.Meta.withoutMVarAssignments {α : Type} (m : Lean.MetaM α) : Lean.MetaM α

Equations

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

def Auto.Meta.inspectMVarAssignments : Lean.MetaM Unit

Equations

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

def Auto.Meta.trySynthInhabited (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Synthesize inhabited instance for a given type

Equations

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

def Auto.fromMetaTactic : Lean.ParserDescr

Equations

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

unsafe def Auto.evalFromMetaTactic : Lean.Elab.Tactic.Tactic

Equations

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

def Auto.Meta.abstractAllMVarFVar (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

def Auto.Meta.coreCheck (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def Auto.Meta.isTypeCorrectCore (e : Lean.Expr) : Lean.MetaM Bool

Equations

• Auto.Meta.isTypeCorrectCore e = do let type? ← Auto.Meta.coreCheck e pure type?.isSome

def Auto.Meta.withMaxHeartbeats {m : Type → Type u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] [MonadWithReaderOf Lean.Core.Context m] (n : Nat) (x : m α) : m α

Equations

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

def Auto.Meta.exToExcept {α : Type} (x : Lean.MetaM α) : Lean.MetaM (Except Lean.Exception α)

Equations

• Auto.Meta.exToExcept x = do let r ← tryCatch (do let v ← x pure (Except.ok v)) fun (e : Lean.Exception) => pure (Except.error e) pure r

def Auto.Meta.runtimeExToExcept {α : Type} (x : Lean.MetaM α) : Lean.MetaM (Except Lean.Exception α)

Equations

• Auto.Meta.runtimeExToExcept x = Lean.tryCatchRuntimeEx (do let v ← x pure (Except.ok v)) fun (e : Lean.Exception) => pure (Except.error e)

def Auto.Meta.Context.modifyLCtx (ctx : Lean.Meta.Context) (lctx : Lean.LocalContext) : Lean.CoreM Lean.Meta.Context

Workaround for modifying the lctx field of Meta.Context

Equations

• Auto.Meta.Context.modifyLCtx ctx lctx = (Lean.Meta.withLCtx' lctx read).run' ctx

def Auto.Meta.Context.modifyLocalInstances (ctx : Lean.Meta.Context) (localInsts : Lean.LocalInstances) : Lean.CoreM Lean.Meta.Context

Workaround for modifying the localInstances field of Meta.Context

Equations

• Auto.Meta.Context.modifyLocalInstances ctx localInsts = (Lean.Meta.withLCtx ctx.lctx localInsts read).run' ctx

def Auto.Meta.replaceNonDep (e p q : Lean.Expr) (occs : Lean.Meta.Occurrences := Lean.Meta.Occurrences.all) : Lean.MetaM Lean.Expr

Replace occurrences of p in non-dependent positions in e with q. The type of the resulting expression should be identical to the type of e · Both e and q are not supposed to contain loose bvars · We detect subterms equivalent to p using key-matching. That is, only perform isDefEq tests when the head symbol of substerm is equivalent to head symbol of p. · We only abstract non-dependent positions That is, if there is a function application f a and the argument of f is dependent, then occurrences of p in a will not be abstracted

By default, all occurrences are abstracted, but this behavior can be controlled using the occs parameter.

All matches of p in e are considered for occurrences, but for each match that is included by the occs parameter, metavariables appearing in p (or e) may become instantiated, affecting the possibility of subsequent matches. For matches that are not included in the occs parameter, the metavariable context is rolled back to prevent blocking subsequent matches which require different instantiations.

Equations

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

partial def Auto.Meta.replaceNonDep.visit (p q : Lean.Expr) (occs : Lean.Meta.Occurrences := Lean.Meta.Occurrences.all) (pHeadIdx : Lean.HeadIndex) (pNumArgs : Nat) (e : Lean.Expr) : StateRefT' IO.RealWorld Nat Lean.MetaM Lean.Expr