opaque auto.mono.saturationThreshold : Lean.Option Nat

opaque auto.mono.recordInstInst : Lean.Option Bool

opaque auto.mono.ciInstDefEq.mode : Lean.Option Lean.Meta.TransparencyMode

opaque auto.mono.ciInstDefEq.maxHeartbeats : Lean.Option Nat

opaque auto.mono.termLikeDefEq.mode : Lean.Option Lean.Meta.TransparencyMode

opaque auto.mono.termLikeDefEq.maxHeartbeats : Lean.Option Nat

inductive Auto.MonoMode : Type

• fol : MonoMode
• hol : MonoMode

instance Auto.instBEqMonoMode : BEq MonoMode

Equations

• Auto.instBEqMonoMode = { beq := Auto.beqMonoMode✝ }

instance Auto.instHashableMonoMode : Hashable MonoMode

Equations

• Auto.instHashableMonoMode = { hash := Auto.hashMonoMode✝ }

instance Auto.instInhabitedMonoMode : Inhabited MonoMode

Equations

• Auto.instInhabitedMonoMode = { default := Auto.MonoMode.fol }

instance Auto.instToStringMonoMode : ToString MonoMode

Equations

• Auto.instToStringMonoMode = { toString := fun (x : Auto.MonoMode) => match x with | Auto.MonoMode.fol => "fol" | Auto.MonoMode.hol => "hol" }

instance Auto.instValueMonoMode : Lean.KVMap.Value MonoMode

Equations

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

opaque auto.mono.mode : Lean.Option Auto.MonoMode

opaque auto.mono.ignoreNonQuasiHigherOrder : Lean.Option Bool

def Auto.Monomorphization.getRecordInstInst : Lean.CoreM Bool

Equations

• Auto.Monomorphization.getRecordInstInst = do let __do_lift ← Lean.getOptions pure (Lean.Option.get __do_lift auto.mono.recordInstInst)

def Auto.Monomorphization.getMode : Lean.CoreM MonoMode

Equations

• Auto.Monomorphization.getMode = do let __do_lift ← Lean.getOptions pure (Lean.Option.get __do_lift auto.mono.mode)

def Auto.Monomorphization.getIgnoreNonQuasiHigherOrder : Lean.CoreM Bool

Equations

• Auto.Monomorphization.getIgnoreNonQuasiHigherOrder = do let __do_lift ← Lean.getOptions pure (Lean.Option.get __do_lift auto.mono.ignoreNonQuasiHigherOrder)

inductive Auto.Monomorphization.CiHead : Type

• fvar : Lean.FVarId → CiHead
• mvar : Lean.MVarId → CiHead
• const : Lean.Name → Array Lean.Level → CiHead

instance Auto.Monomorphization.instInhabitedCiHead : Inhabited CiHead

Equations

• Auto.Monomorphization.instInhabitedCiHead = { default := Auto.Monomorphization.CiHead.fvar default }

instance Auto.Monomorphization.instHashableCiHead : Hashable CiHead

Equations

• Auto.Monomorphization.instHashableCiHead = { hash := Auto.Monomorphization.hashCiHead✝ }

instance Auto.Monomorphization.instBEqCiHead : BEq CiHead

Equations

• Auto.Monomorphization.instBEqCiHead = { beq := Auto.Monomorphization.beqCiHead✝ }

def Auto.Monomorphization.CiHead.ofExpr? : Lean.Expr → Option CiHead

Equations

• Auto.Monomorphization.CiHead.ofExpr? (Lean.Expr.fvar id) = some (Auto.Monomorphization.CiHead.fvar id)
• Auto.Monomorphization.CiHead.ofExpr? (Lean.Expr.mvar id) = some (Auto.Monomorphization.CiHead.mvar id)
• Auto.Monomorphization.CiHead.ofExpr? (Lean.Expr.const name lvls) = some (Auto.Monomorphization.CiHead.const name { toList := lvls })
• Auto.Monomorphization.CiHead.ofExpr? x✝ = none

def Auto.Monomorphization.CiHead.toExpr : CiHead → Lean.Expr

Equations

• (Auto.Monomorphization.CiHead.fvar a).toExpr = Lean.Expr.fvar a
• (Auto.Monomorphization.CiHead.mvar a).toExpr = Lean.Expr.mvar a
• (Auto.Monomorphization.CiHead.const a a_1).toExpr = Lean.Expr.const a a_1.toList

def Auto.Monomorphization.CiHead.fingerPrint : CiHead → Lean.Expr

Ignore constant's levels

Equations

• (Auto.Monomorphization.CiHead.fvar a).fingerPrint = Lean.Expr.fvar a
• (Auto.Monomorphization.CiHead.mvar a).fingerPrint = Lean.Expr.mvar a
• (Auto.Monomorphization.CiHead.const a a_1).fingerPrint = Lean.Expr.const a []

def Auto.Monomorphization.CiHead.isConst : CiHead → Bool

Equations

• (Auto.Monomorphization.CiHead.fvar a).isConst = false
• (Auto.Monomorphization.CiHead.mvar a).isConst = false
• (Auto.Monomorphization.CiHead.const a a_1).isConst = true

def Auto.Monomorphization.CiHead.isNamedConst (name : Lean.Name) : CiHead → Bool

Equations

• Auto.Monomorphization.CiHead.isNamedConst name (Auto.Monomorphization.CiHead.fvar a) = false
• Auto.Monomorphization.CiHead.isNamedConst name (Auto.Monomorphization.CiHead.mvar a) = false
• Auto.Monomorphization.CiHead.isNamedConst name (Auto.Monomorphization.CiHead.const a a_1) = (name == a)

instance Auto.Monomorphization.instToMessageDataCiHead : Lean.ToMessageData CiHead

Equations

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

def Auto.Monomorphization.CiHead.inferType (ci : CiHead) : Lean.MetaM Lean.Expr

Equations

• ci.inferType = Lean.Meta.inferType ci.toExpr

def Auto.Monomorphization.CiHead.isInstanceQuick (ci : CiHead) : Lean.MetaM Bool

Equations

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

def Auto.Monomorphization.CiHead.equiv (ch₁ ch₂ : CiHead) : Lean.MetaM Bool

Remark: This function assigns level mvars if necessary

Equations

• One or more equations did not get rendered due to their size.
• (Auto.Monomorphization.CiHead.fvar a).equiv (Auto.Monomorphization.CiHead.fvar b) = pure (a == b)
• (Auto.Monomorphization.CiHead.mvar a).equiv (Auto.Monomorphization.CiHead.mvar b) = pure (a == b)
• ch₁.equiv ch₂ = pure false

structure Auto.Monomorphization.ConstInst : Type

If a constant c is of type ∀ (xs : αs), t, then its valid instance will be c with all of its universe levels, dependent arguments and instance arguments instantiated. So, we record the instantiation of universe levels and dependent arguments.

As to monomorphization, we will not record instances of constants with instance attribute or whose type is a class.

• head : CiHead
• argsInst : Array Lean.Expr
• argsIdx : Array Nat

instance Auto.Monomorphization.instInhabitedConstInst : Inhabited ConstInst

Equations

• Auto.Monomorphization.instInhabitedConstInst = { default := { head := default, argsInst := default, argsIdx := default } }

instance Auto.Monomorphization.instHashableConstInst : Hashable ConstInst

Equations

• Auto.Monomorphization.instHashableConstInst = { hash := Auto.Monomorphization.hashConstInst✝ }

instance Auto.Monomorphization.instBEqConstInst : BEq ConstInst

Equations

• Auto.Monomorphization.instBEqConstInst = { beq := Auto.Monomorphization.beqConstInst✝ }

def Auto.Monomorphization.ConstInst.fingerPrint (ci : ConstInst) : Lean.Expr

Equations

• ci.fingerPrint = ci.head.fingerPrint

instance Auto.Monomorphization.instToMessageDataConstInst : Lean.ToMessageData ConstInst

Equations

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

def Auto.Monomorphization.ConstInst.equiv (ci₁ ci₂ : ConstInst) : Lean.MetaM Bool

Remark: This function assigns metavariables if necessary, but its only usage in this file is under Meta.withNewMCtxDepth Note that since ci₁, ci₂ are both ConstInst, they does not contain loose bound variables

Equations

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

def Auto.Monomorphization.ConstInst.matchExpr (e : Lean.Expr) (ci : ConstInst) : Lean.MetaM Bool

Remark: · This function assigns metavariables if necessary · Runs in MetaM, so e should not have loose bound variables

Equations

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

def Auto.Monomorphization.ConstInst.ofExpr? (params : Array Lean.Name) (bvars : Array Lean.Expr) (e : Lean.Expr) : Lean.MetaM (Option ConstInst)

Given an hypothesis t, we will traverse the hypothesis and call ConstInst.ofExpr? to find instances of polymorphic constants

· Binders of the hypothesis are introduced as fvars, these fvars are recorded in bvars

· param records universe level parameters of the hypothesis

So, the criterion that an expression e is a valid instance is that · All dependent arguments and instance arguments are present

· The head does not contain expressions in bvars

· Dependent arguments does not contains expressions in bvars

· The expression does not contain level parameters in params

Equations

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

def Auto.Monomorphization.ConstInst.ofExpr?.shouldInstantiate (fn ty body : Lean.Expr) (bi : Lean.BinderInfo) : Lean.CoreM Bool

Equations

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

def Auto.Monomorphization.ConstInst.toExpr (ci : ConstInst) : Lean.MetaM Lean.Expr

Equations

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

def Auto.Monomorphization.ConstInst.getOtherArgs (ci : ConstInst) (e : Lean.Expr) : Lean.CoreM (Array Lean.Expr)

Precondition : .some ci == ← ConstInst.ofExpr? e Returns the list of non-dependent arguments in e.getAppArgs

Equations

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

@[reducible, inline]

abbrev Auto.Monomorphization.ConstInsts : Type

Array of instances of a polymorphic constant

Equations

• Auto.Monomorphization.ConstInsts = Array Auto.Monomorphization.ConstInst

def Auto.Monomorphization.ConstInsts.canonicalize? (cis : ConstInsts) (ci : ConstInst) : Lean.MetaM (Option ConstInst)

Given an array cis and a potentially new instance ci · If ci is new, add it to ConstInsts and return true · If ci is not new, return an element of the original ConstInsts which is definitionally equal to ci

Equations

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

def Auto.Monomorphization.LemmaInst.matchConstInst (ci : ConstInst) (li : LemmaInst) : Lean.MetaM (Std.HashSet LemmaInst)

Given a LemmaInst li and a ConstInst ci, try to match all subexpressions of li against ci

Equations

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

def Auto.Monomorphization.leadingForallQuasiMonomorphic (e : Lean.Expr) : Lean.MetaM Bool

Check whether the leading ∀ quantifiers of expression e violates the quasi-monomorphic condition

Equations

• Auto.Monomorphization.leadingForallQuasiMonomorphic = Auto.Monomorphization.leadingForallQuasiMonomorphic.leadingForallQuasiMonomorphicAux #[]

partial def Auto.Monomorphization.leadingForallQuasiMonomorphic.leadingForallQuasiMonomorphicAux (fvars : Array Lean.FVarId) (e : Lean.Expr) : Lean.MetaM Bool

def Auto.Monomorphization.LemmaInst.monomorphic? (li : LemmaInst) : Lean.MetaM (Option LemmaInst)

Test whether a lemma is type monomorphic && universe monomorphic By universe monomorphic we mean lem.params = #[] If all dependent arguments are instantiated, but some instance arguments are not instantiated, we will try to synthesize the instance arguments

Equations

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

structure Auto.Monomorphization.State : Type

Monomorphization works as follows:

(1) Turning Lemmas into LemmaInsts, which constitutes the value of lisArr in the beginning

(2) Scan through all assumptions to find subterms that are valid instances of constants (dependent arguments fully instantiated). They form the initial elements of ciMap and activeCi

(3) Repeat:

· Dequeue an element active

· If it is a ConstInst, match against all existing LemmaInst; If it is a LemmaInst, match against all existing ConstInst

· For all the new LemmaInsts generated and all the ConstInsts occurring in them to active

• ciMap : Std.HashMap Lean.Expr ConstInsts
• lisArr : Array LemmaInsts
• ciInstDefEqs : Array LemmaInst
• active : Std.Queue (ConstInst ⊕ LemmaInst × Nat)

@[reducible, inline]

abbrev Auto.Monomorphization.MonoM (α : Type) : Type

Equations

• Auto.Monomorphization.MonoM = StateRefT' IO.RealWorld Auto.Monomorphization.State Lean.MetaM

def Auto.Monomorphization.getLisArr : MonoM (Array LemmaInsts)

Equations

• Auto.Monomorphization.getLisArr = do let st ← get pure st.lisArr

def Auto.Monomorphization.setActive (field : Std.Queue (ConstInst ⊕ LemmaInst × Nat)) : MonoM PUnit

Equations

• Auto.Monomorphization.setActive field = modify fun (st : Auto.Monomorphization.State) => { ciMap := st.ciMap, lisArr := st.lisArr, ciInstDefEqs := st.ciInstDefEqs, active := field }

def Auto.Monomorphization.getCiMap : MonoM (Std.HashMap Lean.Expr ConstInsts)

Equations

• Auto.Monomorphization.getCiMap = do let st ← get pure st.ciMap

def Auto.Monomorphization.getCiInstDefEqs : MonoM (Array LemmaInst)

Equations

• Auto.Monomorphization.getCiInstDefEqs = do let st ← get pure st.ciInstDefEqs

def Auto.Monomorphization.setCiMap (field : Std.HashMap Lean.Expr ConstInsts) : MonoM PUnit

Equations

• Auto.Monomorphization.setCiMap field = modify fun (st : Auto.Monomorphization.State) => { ciMap := field, lisArr := st.lisArr, ciInstDefEqs := st.ciInstDefEqs, active := st.active }

def Auto.Monomorphization.getActive : MonoM (Std.Queue (ConstInst ⊕ LemmaInst × Nat))

Equations

• Auto.Monomorphization.getActive = do let st ← get pure st.active

def Auto.Monomorphization.setLisArr (field : Array LemmaInsts) : MonoM PUnit

Equations

• Auto.Monomorphization.setLisArr field = modify fun (st : Auto.Monomorphization.State) => { ciMap := st.ciMap, lisArr := field, ciInstDefEqs := st.ciInstDefEqs, active := st.active }

def Auto.Monomorphization.setCiInstDefEqs (field : Array LemmaInst) : MonoM PUnit

Equations

• Auto.Monomorphization.setCiInstDefEqs field = modify fun (st : Auto.Monomorphization.State) => { ciMap := st.ciMap, lisArr := st.lisArr, ciInstDefEqs := field, active := st.active }

def Auto.Monomorphization.CiMap.canonicalize? (ciMap : Std.HashMap Lean.Expr ConstInsts) (ci : ConstInst) : Lean.MetaM (Bool × ConstInsts × ConstInst)

Equations

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

def Auto.Monomorphization.processConstInst (ci : ConstInst) : MonoM Unit

Process a potentially new ConstInst. If it's new, return its index in the corresponding ConstInsts array. If it's not new, return .none.

Equations

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

partial def Auto.Monomorphization.termLikeSubexprs (bvars : Array Lean.Expr) : Lean.Expr → Lean.MetaM (Array Lean.Expr)

def Auto.Monomorphization.termLikeDefEqDefEqs (lemmas : Array Lemma) : Lean.MetaM (Array Lemma)

Equations

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

def Auto.Monomorphization.termLikeDefEqDefEqs.isTrivialEq (e : Lean.Expr) : Lean.MetaM Bool

Equations

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

def Auto.Monomorphization.initializeMonoM (lemmas : Array Lemma) : MonoM Unit

Equations

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

def Auto.Monomorphization.dequeueActive? : MonoM (Option (ConstInst ⊕ LemmaInst × Nat))

Equations

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

def Auto.Monomorphization.lookupActiveCi! (fgp : Lean.Expr) (idx : Nat) : MonoM ConstInst

Equations

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

def Auto.Monomorphization.saturationThresholdReached? (cnt : Nat) : Lean.CoreM Bool

Equations

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

def Auto.Monomorphization.saturate : MonoM Unit

Monomorphization works as follows:

(1) Turning Lemmas into LemmaInsts, which constitutes the value of lisArr in the beginning

(2) Scan through all assumptions to find subterms that are valid instances of constants (dependent arguments fully instantiated). They form the initial elements of ciMap and activeCi

(3) Repeat:

· Dequeue an element active

· If it is a ConstInst, match against all existing LemmaInst; If it is a LemmaInst, match against all existing ConstInst

· For all the new LemmaInsts generated and all the ConstInsts occurring in them to active

Equations

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

def Auto.Monomorphization.saturate.matchCiAndLi (ci : ConstInst) (li : LemmaInst) (idx cnt : Nat) : MonoM (LemmaInsts × Nat)

Equations

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

def Auto.Monomorphization.saturate.generateCiInstDefEq (ci : ConstInst) : MonoM Unit

Equations

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

def Auto.Monomorphization.saturate.collectAndProcessConstInsts (li : LemmaInst) : MonoM Unit

Equations

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

def Auto.Monomorphization.saturate.bidirectionalOfInstanceEq (ci₁ ci₂ : ConstInst) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Array Lean.Name))

Equations

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

def Auto.Monomorphization.saturate.isTrigger (cih : CiHead) : Bool

Equations

• Auto.Monomorphization.saturate.isTrigger (Auto.Monomorphization.CiHead.const name a) = (name == `Auto.SMT.Attribute.trigger)
• Auto.Monomorphization.saturate.isTrigger cih = false

def Auto.Monomorphization.getAllMonoLemmaInsts : MonoM LemmaInsts

Remove non-monomorphic lemma instances

Equations

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

def Auto.Monomorphization.collectMonoMutInds : MonoM (Array (Array SimpleIndVal))

Collect inductive types

Equations

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

structure Auto.Monomorphization.FVarRep.State : Type

• bfvars : Array Lean.FVarId
• ffvars : Array Lean.FVarId
• exprMap : Std.HashMap Lean.Expr Lean.FVarId
• ciMap : Std.HashMap Lean.Expr ConstInsts
• ciIdMap : Std.HashMap ConstInst Lean.FVarId
• idCiMap : Std.HashMap Lean.FVarId ConstInst
• tyCanMap : Std.HashMap Lean.Expr Lean.Expr

@[reducible, inline]

abbrev Auto.Monomorphization.FVarRep.FVarRepM (α : Type) : Type

Equations

• Auto.Monomorphization.FVarRep.FVarRepM = StateRefT' IO.RealWorld Auto.Monomorphization.FVarRep.State Auto.MetaState.MetaStateM

def Auto.Monomorphization.FVarRep.setFfvars (field : Array Lean.FVarId) : FVarRepM PUnit

Equations

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

def Auto.Monomorphization.FVarRep.getFfvars : FVarRepM (Array Lean.FVarId)

Equations

• Auto.Monomorphization.FVarRep.getFfvars = do let st ← get pure st.ffvars

def Auto.Monomorphization.FVarRep.getExprMap : FVarRepM (Std.HashMap Lean.Expr Lean.FVarId)

Equations

• Auto.Monomorphization.FVarRep.getExprMap = do let st ← get pure st.exprMap

def Auto.Monomorphization.FVarRep.setTyCanMap (field : Std.HashMap Lean.Expr Lean.Expr) : FVarRepM PUnit

Equations

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

def Auto.Monomorphization.FVarRep.setCiMap (field : Std.HashMap Lean.Expr ConstInsts) : FVarRepM PUnit

Equations

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

def Auto.Monomorphization.FVarRep.setExprMap (field : Std.HashMap Lean.Expr Lean.FVarId) : FVarRepM PUnit

Equations

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

def Auto.Monomorphization.FVarRep.getIdCiMap : FVarRepM (Std.HashMap Lean.FVarId ConstInst)

Equations

• Auto.Monomorphization.FVarRep.getIdCiMap = do let st ← get pure st.idCiMap

def Auto.Monomorphization.FVarRep.getCiMap : FVarRepM (Std.HashMap Lean.Expr ConstInsts)

Equations

• Auto.Monomorphization.FVarRep.getCiMap = do let st ← get pure st.ciMap

def Auto.Monomorphization.FVarRep.getBfvars : FVarRepM (Array Lean.FVarId)

Equations

• Auto.Monomorphization.FVarRep.getBfvars = do let st ← get pure st.bfvars

def Auto.Monomorphization.FVarRep.setCiIdMap (field : Std.HashMap ConstInst Lean.FVarId) : FVarRepM PUnit

Equations

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

def Auto.Monomorphization.FVarRep.getCiIdMap : FVarRepM (Std.HashMap ConstInst Lean.FVarId)

Equations

• Auto.Monomorphization.FVarRep.getCiIdMap = do let st ← get pure st.ciIdMap

def Auto.Monomorphization.FVarRep.setIdCiMap (field : Std.HashMap Lean.FVarId ConstInst) : FVarRepM PUnit

Equations

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

def Auto.Monomorphization.FVarRep.getTyCanMap : FVarRepM (Std.HashMap Lean.Expr Lean.Expr)

Equations

• Auto.Monomorphization.FVarRep.getTyCanMap = do let st ← get pure st.tyCanMap

def Auto.Monomorphization.FVarRep.setBfvars (field : Array Lean.FVarId) : FVarRepM PUnit

Equations

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

def Auto.Monomorphization.FVarRep.getBfvarSet : FVarRepM (Std.HashSet Lean.FVarId)

Equations

• Auto.Monomorphization.FVarRep.getBfvarSet = do let bfvars ← Auto.Monomorphization.FVarRep.getBfvars pure (Std.HashSet.emptyWithCapacity.insertMany bfvars)

def Auto.Monomorphization.FVarRep.getFfvarSet : FVarRepM (Std.HashSet Lean.FVarId)

Equations

• Auto.Monomorphization.FVarRep.getFfvarSet = do let ffvars ← Auto.Monomorphization.FVarRep.getFfvars pure (Std.HashSet.emptyWithCapacity.insertMany ffvars)

def Auto.Monomorphization.FVarRep.processConstInst (ci : ConstInst) : FVarRepM Unit

Similar to Monomorphization.processConstInst

Equations

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

def Auto.Monomorphization.FVarRep.processType (e : Lean.Expr) : FVarRepM (Lean.Expr × Bool)

Return : (reduce(e), whether reduce(e) contain bfvars)

Equations

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

def Auto.Monomorphization.FVarRep.processType.processTypeAux : Lean.Expr → FVarRepM Unit

Equations

• One or more equations did not get rendered due to their size.
• Auto.Monomorphization.FVarRep.processType.processTypeAux x✝ = Auto.Monomorphization.FVarRep.processType.addTypeToTyCanMap x✝

def Auto.Monomorphization.FVarRep.processType.addTypeToTyCanMap (e : Lean.Expr) : FVarRepM Unit

Equations

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

def Auto.Monomorphization.FVarRep.constInst2FVarId (ci : ConstInst) : FVarRepM Lean.FVarId

Equations

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

def Auto.Monomorphization.FVarRep.monoFailMsg (e : Lean.Expr) : Lean.MessageData

Equations

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

def Auto.Monomorphization.FVarRep.unknownExpr2FVar (e : Lean.Expr) : FVarRepM (Lean.Expr ⊕ Lean.MessageData)

Equations

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

partial def Auto.Monomorphization.FVarRep.replacePolyWithFVar : Lean.Expr → FVarRepM (Lean.Expr ⊕ Lean.MessageData)

Attempt to abstract parts of a given expression to free variables so that the resulting expression is in the higher-order fragment of Lean.

Note that it's not always possible to do this since it's possible that the given expression itself is polymorphic

Since we're now dealing with monomorphized lemmas, there are no bound level parameters

Return value:

· If abstraction is successful, return the abstracted expression

· If abstraction is not successful because the input is not a quasi higher-order

term of type Prop, return a message indicating the violation of quasi higher-order-ness · Throw an error message if unexpected error happens

def Auto.Monomorphization.FVarRep.replacePolyWithFVar.addForallImpFInst (e : Lean.Expr) : FVarRepM Unit

Equations

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

def Auto.Monomorphization.intromono (lemmas : Array Lemma) (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Given mvarId : ty, create a fresh mvar m of type monofact₁ → monofact₂ → ⋯ → monofactₙ → ty and return (m proof₁ proof₂ ⋯ proofₙ, m)

Equations

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

def Auto.Monomorphization.monomorphize {α : Type} (lemmas inhFacts : Array Lemma) (k : Reif.State → Lean.MetaM α) : Lean.MetaM α

Equations

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

def Auto.Monomorphization.monomorphize.monoMAction (lemmas : Array Lemma) : MonoM (LemmaInsts × Array (Array SimpleIndVal))

Instantiating quantifiers, collecting inductive types and filtering out non-quasi-monomorphic expressions

Equations

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

def Auto.Monomorphization.monomorphize.metaStateMAction (inhFacts : Array Lemma) (monoLemmas : LemmaInsts) (monoIndVals : Array (Array SimpleIndVal)) (monoSt : State) : MetaState.MetaStateM (Array Lean.FVarId × Reif.State)

Process lemmas and inductive types, collect inhabited types

Equations

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

def Auto.Monomorphization.monomorphize.fvarRepMFactAction (lis : Array LemmaInst) : FVarRep.FVarRepM (Array UMonoFact)

Equations

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

def Auto.Monomorphization.monomorphize.fvarRepMInductAction (ivals : Array (Array SimpleIndVal)) : FVarRep.FVarRepM (Array (Array SimpleIndVal))

Equations

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