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