def Auto.Expr.eraseMData : Lean.Expr → Lean.Expr

Equations

• Auto.Expr.eraseMData (fn.app arg) = (Auto.Expr.eraseMData fn).app (Auto.Expr.eraseMData arg)
• Auto.Expr.eraseMData (Lean.Expr.lam name ty body bi) = Lean.Expr.lam name (Auto.Expr.eraseMData ty) (Auto.Expr.eraseMData body) bi
• Auto.Expr.eraseMData (Lean.Expr.forallE name ty body bi) = Lean.Expr.forallE name (Auto.Expr.eraseMData ty) (Auto.Expr.eraseMData body) bi
• Auto.Expr.eraseMData (Lean.Expr.letE name type value body nonDep) = Lean.Expr.letE name (Auto.Expr.eraseMData type) (Auto.Expr.eraseMData value) (Auto.Expr.eraseMData body) nonDep
• Auto.Expr.eraseMData (Lean.Expr.mdata data expr) = expr
• Auto.Expr.eraseMData (Lean.Expr.proj typeName idx struct) = Lean.Expr.proj typeName idx (Auto.Expr.eraseMData struct)
• Auto.Expr.eraseMData x✝ = x✝

def Auto.Expr.hasCurrentDepthLevelMVar : Lean.Expr → Lean.MetaM Bool

Equations

• One or more equations did not get rendered due to their size.
• Auto.Expr.hasCurrentDepthLevelMVar (Lean.Expr.sort l) = Auto.Level.hasCurrentDepthLevelMVar l
• Auto.Expr.hasCurrentDepthLevelMVar (Lean.Expr.const declName ls) = List.anyM Auto.Level.hasCurrentDepthLevelMVar ls
• Auto.Expr.hasCurrentDepthLevelMVar (Lean.Expr.forallE binderName d b binderInfo) = or <$> Auto.Expr.hasCurrentDepthLevelMVar d <*> Auto.Expr.hasCurrentDepthLevelMVar b
• Auto.Expr.hasCurrentDepthLevelMVar (Lean.Expr.lam binderName d b binderInfo) = or <$> Auto.Expr.hasCurrentDepthLevelMVar d <*> Auto.Expr.hasCurrentDepthLevelMVar b
• Auto.Expr.hasCurrentDepthLevelMVar (f.app a) = or <$> Auto.Expr.hasCurrentDepthLevelMVar f <*> Auto.Expr.hasCurrentDepthLevelMVar a
• Auto.Expr.hasCurrentDepthLevelMVar (Lean.Expr.mdata data b) = Auto.Expr.hasCurrentDepthLevelMVar b
• Auto.Expr.hasCurrentDepthLevelMVar (Lean.Expr.proj typeName idx e) = Auto.Expr.hasCurrentDepthLevelMVar e
• Auto.Expr.hasCurrentDepthLevelMVar x✝ = pure false

def Auto.Expr.findParam? (p : Lean.Name → Bool) : Lean.Expr → Option Lean.Name

Equations

• Auto.Expr.findParam? p (Lean.Expr.sort l) = Auto.Level.findParam? p l
• Auto.Expr.findParam? p (Lean.Expr.const declName ls) = List.foldl (fun (acc : Option Lean.Name) (x : Lean.Level) => acc.orElse fun (x_1 : Unit) => Auto.Level.findParam? p x) none ls
• Auto.Expr.findParam? p (Lean.Expr.forallE binderName d b binderInfo) = (Auto.Expr.findParam? p d).orElse fun (x : Unit) => Auto.Expr.findParam? p b
• Auto.Expr.findParam? p (Lean.Expr.lam binderName d b binderInfo) = (Auto.Expr.findParam? p d).orElse fun (x : Unit) => Auto.Expr.findParam? p b
• Auto.Expr.findParam? p (Lean.Expr.letE declName t v b nonDep) = (Auto.Expr.findParam? p t).orElse fun (x : Unit) => (Auto.Expr.findParam? p v).orElse fun (x : Unit) => Auto.Expr.findParam? p b
• Auto.Expr.findParam? p (f.app a) = (Auto.Expr.findParam? p f).orElse fun (x : Unit) => Auto.Expr.findParam? p a
• Auto.Expr.findParam? p (Lean.Expr.mdata data b) = Auto.Expr.findParam? p b
• Auto.Expr.findParam? p (Lean.Expr.proj typeName idx e) = Auto.Expr.findParam? p e
• Auto.Expr.findParam? p x✝ = none

def Auto.Expr.forallBinders (e : Lean.Expr) : Array (Lean.Name × Lean.Expr × Lean.BinderInfo)

Equations

• Auto.Expr.forallBinders e = { toList := Auto.Expr.forallBinders.aux e }

def Auto.Expr.forallBinders.aux (e : Lean.Expr) : List (Lean.Name × Lean.Expr × Lean.BinderInfo)

Equations

• Auto.Expr.forallBinders.aux (Lean.Expr.forallE n ty b bi) = (n, ty, bi) :: Auto.Expr.forallBinders.aux b
• Auto.Expr.forallBinders.aux e = []

def Auto.Expr.collectRawM {m : Type → Type u_1} [Monad m] (p : Lean.Expr → m Bool) : Lean.Expr → m (Std.HashSet Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.
• Auto.Expr.collectRawM p (f.app a) = do let hf ← Auto.Expr.collectRawM p f let ha ← Auto.Expr.collectRawM p a Auto.Expr.collectRawM.addp? p (f.app a) (Auto.mergeHashSet hf ha)
• Auto.Expr.collectRawM p (Lean.Expr.mdata data b) = do let hb ← Auto.Expr.collectRawM p b Auto.Expr.collectRawM.addp? p (Lean.Expr.mdata data b) hb
• Auto.Expr.collectRawM p (Lean.Expr.proj typeName idx b) = do let hb ← Auto.Expr.collectRawM p b Auto.Expr.collectRawM.addp? p (Lean.Expr.proj typeName idx b) hb
• Auto.Expr.collectRawM p x✝ = Auto.Expr.collectRawM.addp? p x✝ Std.HashSet.emptyWithCapacity

def Auto.Expr.collectRawM.addp? {m : Type → Type u_1} [Monad m] (p : Lean.Expr → m Bool) (e : Lean.Expr) (hs : Std.HashSet Lean.Expr) : m (Std.HashSet Lean.Expr)

Equations

• Auto.Expr.collectRawM.addp? p e hs = do let __do_lift ← p e if __do_lift = true then pure (hs.insert e) else pure hs

def Auto.Expr.lambdaBinders (e : Lean.Expr) : Array (Lean.Name × Lean.Expr × Lean.BinderInfo)

Equations

• Auto.Expr.lambdaBinders e = { toList := Auto.Expr.lambdaBinders.aux e }

def Auto.Expr.lambdaBinders.aux (e : Lean.Expr) : List (Lean.Name × Lean.Expr × Lean.BinderInfo)

Equations

• Auto.Expr.lambdaBinders.aux (Lean.Expr.lam n ty b bi) = (n, ty, bi) :: Auto.Expr.lambdaBinders.aux b
• Auto.Expr.lambdaBinders.aux e = []

def Auto.Expr.isDepForall (e : Lean.Expr) : Bool

Equations

• Auto.Expr.isDepForall (Lean.Expr.forallE n ty b bi) = b.hasLooseBVar 0
• Auto.Expr.isDepForall e = false

def Auto.Expr.isDepLambda (e : Lean.Expr) : Bool

Equations

• Auto.Expr.isDepLambda (Lean.Expr.lam n ty b bi) = b.hasLooseBVar 0
• Auto.Expr.isDepLambda e = false

def Auto.Expr.mkForallFromBinderDescrs (binders : Array (Lean.Name × Lean.Expr × Lean.BinderInfo)) (e : Lean.Expr) : Lean.Expr

Equations

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

def Auto.Expr.mkLambdaFromBinderDescrs (binders : Array (Lean.Name × Lean.Expr × Lean.BinderInfo)) (e : Lean.Expr) : Lean.Expr

Equations

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

def Auto.Expr.stripForall (e : Lean.Expr) : Lean.Expr

Equations

• Auto.Expr.stripForall (Lean.Expr.forallE n ty b bi) = Auto.Expr.stripForall b
• Auto.Expr.stripForall e = e

def Auto.Expr.stripLeadingDepForall (e : Lean.Expr) : Lean.Expr

Equations

• Auto.Expr.stripLeadingDepForall (Lean.Expr.forallE n ty b bi) = if b.hasLooseBVar 0 = true then Auto.Expr.stripLeadingDepForall b else Lean.Expr.forallE n ty b bi
• Auto.Expr.stripLeadingDepForall e = e

def Auto.Expr.stripForallN (n : Nat) (e : Lean.Expr) : Option Lean.Expr

Equations

• Auto.Expr.stripForallN 0 e = some e
• Auto.Expr.stripForallN n'.succ (Lean.Expr.forallE n ty b bi) = Auto.Expr.stripForallN n' b
• Auto.Expr.stripForallN n'.succ e = none

def Auto.Expr.stripLambda (e : Lean.Expr) : Lean.Expr

Equations

• Auto.Expr.stripLambda (Lean.Expr.lam n ty b bi) = Auto.Expr.stripLambda b
• Auto.Expr.stripLambda e = e

def Auto.Expr.stripLeadingDepLambda (e : Lean.Expr) : Lean.Expr

Equations

• Auto.Expr.stripLeadingDepLambda (Lean.Expr.lam n ty b bi) = if b.hasLooseBVar 0 = true then Auto.Expr.stripLeadingDepLambda b else Lean.Expr.lam n ty b bi
• Auto.Expr.stripLeadingDepLambda e = e

def Auto.Expr.stripLambdaN (n : Nat) (e : Lean.Expr) : Option Lean.Expr

Equations

• Auto.Expr.stripLambdaN 0 e = some e
• Auto.Expr.stripLambdaN n'.succ (Lean.Expr.lam n ty b bi) = Auto.Expr.stripLambdaN n' b
• Auto.Expr.stripLambdaN n'.succ e = none

def Auto.Expr.getAppFnN (n : Nat) (e : Lean.Expr) : Option Lean.Expr

Equations

• Auto.Expr.getAppFnN 0 e = some e
• Auto.Expr.getAppFnN n'.succ (fn.app arg) = Auto.Expr.getAppFnN n' fn
• Auto.Expr.getAppFnN n'.succ e = none

def Auto.Expr.getAppBoundedArgs (n : Nat) (e : Lean.Expr) : Array Lean.Expr

Equations

• Auto.Expr.getAppBoundedArgs n e = { toList := (Auto.Expr.getAppBoundedArgsAux✝ n e).reverse }

def Auto.Expr.instArgs (e : Lean.Expr) : Array Nat

Given an expression e, which is the type of some term t, find the arguments of t that are class instances

Equations

• Auto.Expr.instArgs e = { toList := Auto.Expr.instArgsIdx✝ e 0 }

def Auto.Expr.depArgs (e : Lean.Expr) : Array Nat

Given e = ∀ (xs : αs), t, return the indexes of dependent ∀ binders within xs. This function only works for expressions that does not contain loose bound variables

Equations

• Auto.Expr.depArgs e = { toList := Auto.Expr.depArgsIdx✝ e 0 }

def Auto.Expr.constDepArgs (c : Lean.Name) : Lean.CoreM (Array Nat)

Given the name c of a constant, suppose @c : ty, return Expr.depArgs ty

Equations

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

def Auto.Expr.numLeadingDepArgs : Lean.Expr → Nat

Equations

• Auto.Expr.numLeadingDepArgs (Lean.Expr.forallE n ty b bi) = if b.hasLooseBVar 0 = true then Auto.Expr.numLeadingDepArgs b + 1 else 0
• Auto.Expr.numLeadingDepArgs x✝ = 0

def Auto.Expr.normalizeType (ty : Lean.Expr) : Lean.MetaM Lean.Expr

This should only be used when we're sure that reducing ty won't be too expensive e.g. ty must be defeq to Expr.sort <?lvl>

Equations

• Auto.Expr.normalizeType ty = do let ty ← Lean.Meta.reduceAll ty let __do_lift ← Lean.instantiateMVars ty pure __do_lift

def Auto.Expr.whnfIfNotForall (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Auto.Expr.whnfIfNotForall e = if e.isForall = true then pure e else do let __do_lift ← Lean.Meta.whnf e pure __do_lift

def Auto.Expr.instanceOf? (e₁ : Lean.Expr) (params : Array Lean.Name) (e₂ : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Array Lean.Name))

Given expression e₁, e₂ where e₁ have universe level parameters params, attempt to find variables x₁, ⋯, xₗ, terms t₁, ⋯, tₖ and a m ≤ l such that ∀ x₁ ⋯ xₗ. e₁ t₁ ⋯ tₖ = e₂ x₁ ⋯ xₘ Note that universe polymorphism is not supported

If successful, return (fun x₁ ⋯ xₗ => Eq.refl (e₂ x₁ ⋯ xₘ), ∀ x₁ ⋯ xₗ. e₁ t₁ ⋯ tₖ = e₂ x₁ ⋯ xₘ)

Otherwise, return .none

Equations

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

def Auto.Expr.formatWithUsername (e : Lean.Expr) : Lean.MetaM Std.Format

Equations

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

def Auto.getExprAndApply : Lean.ParserDescr

ident must be of type Expr → TermElabM Unit Compiles term into Expr, then applies ident to it

Equations

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

unsafe def Auto.elabGetExprAndApply : Lean.Elab.Command.CommandElab

Equations

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

unsafe def Auto.exprFromExpr (eToExpr : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Consider the canonical instance of Lean.ToExpr Expr. We require that (← exprFromExpr (← Lean.toExpr e)) ≝ e

Equations

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

def Auto.lazyReduce : Lean.ParserDescr

Equations

• Auto.lazyReduce = Lean.ParserDescr.node `Auto.lazyReduce 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#lazyReduce") (Lean.ParserDescr.cat `term 0))

opaque Auto.lazyReduce.skipProof : Lean.Option Bool

opaque Auto.lazyReduce.skipType : Lean.Option Bool

opaque Auto.lazyReduce.logInfo : Lean.Option Bool

opaque Auto.lazyReduce.printTime : Lean.Option Bool

def Auto.elabLazyReduce : Lean.Elab.Command.CommandElab

Equations

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