structure Auto.LamReif.State : Type

We require that all instances of polymorphic constants, including ∀, ∃, BitVec, are turned into free variables before being sent to LamReif. Since propositional implication → has the same representation as ∀ in Lean Expr, we also require that they are turned into free variables. In this way, the expression that LamReif receives is an essentially higher-order term that can be reified directly.

• tyVarMap : Std.HashMap Lean.Expr Nat
• varMap : Std.HashMap Lean.Expr Nat
• tyVal : Array (Lean.Expr × Lean.Level)
• varVal : Array (Lean.Expr × Embedding.Lam.LamSort)
• lamILTy : Array Embedding.Lam.LamSort
• isomTyMap : Std.HashMap Embedding.Lam.LamSort Nat
• assertions : Std.HashMap Embedding.Lam.LamTerm (Lean.Expr × DTr × Embedding.Lam.LamTerm × Nat)
• inhabitations : Std.HashMap Embedding.Lam.LamSort (Lean.Expr × DTr × Nat)
• chkStepCache : Std.HashMap Embedding.Lam.ChkStep (Embedding.Lam.EvalResult × Array Nat)
• etomChkStep : Std.HashMap Nat Embedding.Lam.ChkStep
• rst : Embedding.Lam.RTableStatus
• u : Lean.Level

def Auto.LamReif.instInhabitedState.default : State

Equations

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

instance Auto.LamReif.instInhabitedState : Inhabited State

Equations

• Auto.LamReif.instInhabitedState = { default := Auto.LamReif.instInhabitedState.default }

@[reducible, inline]

abbrev Auto.LamReif.ReifM (α : Type) : Type

Equations

• Auto.LamReif.ReifM = StateRefT' IO.RealWorld Auto.LamReif.State Auto.Reif.ReifM

@[inline]

def Auto.LamReif.ReifM.run' {α : Type} (x : ReifM α) (s : State) : Reif.ReifM α

Equations

• x.run' s = Prod.fst <$> StateRefT'.run x s

def Auto.LamReif.setAssertions (field : Std.HashMap Embedding.Lam.LamTerm (Lean.Expr × DTr × Embedding.Lam.LamTerm × Nat)) : ReifM PUnit

Equations

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

def Auto.LamReif.setLamILTy (field : Array Embedding.Lam.LamSort) : ReifM PUnit

Equations

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

def Auto.LamReif.setU (field : Lean.Level) : ReifM PUnit

Equations

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

def Auto.LamReif.getLamILTy : ReifM (Array Embedding.Lam.LamSort)

Equations

• Auto.LamReif.getLamILTy = do let st ← get pure st.lamILTy

def Auto.LamReif.getAssertions : ReifM (Std.HashMap Embedding.Lam.LamTerm (Lean.Expr × DTr × Embedding.Lam.LamTerm × Nat))

Equations

• Auto.LamReif.getAssertions = do let st ← get pure st.assertions

def Auto.LamReif.getInhabitations : ReifM (Std.HashMap Embedding.Lam.LamSort (Lean.Expr × DTr × Nat))

Equations

• Auto.LamReif.getInhabitations = do let st ← get pure st.inhabitations

def Auto.LamReif.getTyVarMap : ReifM (Std.HashMap Lean.Expr Nat)

Equations

• Auto.LamReif.getTyVarMap = do let st ← get pure st.tyVarMap

def Auto.LamReif.setTyVarMap (field : Std.HashMap Lean.Expr Nat) : ReifM PUnit

Equations

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

def Auto.LamReif.getChkStepCache : ReifM (Std.HashMap Embedding.Lam.ChkStep (Embedding.Lam.EvalResult × Array Nat))

Equations

• Auto.LamReif.getChkStepCache = do let st ← get pure st.chkStepCache

def Auto.LamReif.setVarVal (field : Array (Lean.Expr × Embedding.Lam.LamSort)) : ReifM PUnit

Equations

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

def Auto.LamReif.setChkStepCache (field : Std.HashMap Embedding.Lam.ChkStep (Embedding.Lam.EvalResult × Array Nat)) : ReifM PUnit

Equations

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

def Auto.LamReif.setVarMap (field : Std.HashMap Lean.Expr Nat) : ReifM PUnit

Equations

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

def Auto.LamReif.setEtomChkStep (field : Std.HashMap Nat Embedding.Lam.ChkStep) : ReifM PUnit

Equations

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

def Auto.LamReif.getVarVal : ReifM (Array (Lean.Expr × Embedding.Lam.LamSort))

Equations

• Auto.LamReif.getVarVal = do let st ← get pure st.varVal

def Auto.LamReif.getIsomTyMap : ReifM (Std.HashMap Embedding.Lam.LamSort Nat)

Equations

• Auto.LamReif.getIsomTyMap = do let st ← get pure st.isomTyMap

def Auto.LamReif.getU : ReifM Lean.Level

Equations

• Auto.LamReif.getU = do let st ← get pure st.u

def Auto.LamReif.getRst : ReifM Embedding.Lam.RTableStatus

Equations

• Auto.LamReif.getRst = do let st ← get pure st.rst

def Auto.LamReif.getVarMap : ReifM (Std.HashMap Lean.Expr Nat)

Equations

• Auto.LamReif.getVarMap = do let st ← get pure st.varMap

def Auto.LamReif.setTyVal (field : Array (Lean.Expr × Lean.Level)) : ReifM PUnit

Equations

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

def Auto.LamReif.setRst (field : Embedding.Lam.RTableStatus) : ReifM PUnit

Equations

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

def Auto.LamReif.getTyVal : ReifM (Array (Lean.Expr × Lean.Level))

Equations

• Auto.LamReif.getTyVal = do let st ← get pure st.tyVal

def Auto.LamReif.setIsomTyMap (field : Std.HashMap Embedding.Lam.LamSort Nat) : ReifM PUnit

Equations

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

def Auto.LamReif.getEtomChkStep : ReifM (Std.HashMap Nat Embedding.Lam.ChkStep)

Equations

• Auto.LamReif.getEtomChkStep = do let st ← get pure st.etomChkStep

def Auto.LamReif.setInhabitations (field : Std.HashMap Embedding.Lam.LamSort (Lean.Expr × DTr × Nat)) : ReifM PUnit

Equations

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

def Auto.LamReif.getRTable : ReifM (Array Embedding.Lam.REntry)

Equations

• Auto.LamReif.getRTable = do let __do_lift ← Auto.LamReif.getRst pure __do_lift.rTable

def Auto.LamReif.getRTableTree : ReifM (BinTree Embedding.Lam.REntry)

Equations

• Auto.LamReif.getRTableTree = do let __do_lift ← Auto.LamReif.getRst pure __do_lift.rTableTree

def Auto.LamReif.getMaxEVarSucc : ReifM Nat

Equations

• Auto.LamReif.getMaxEVarSucc = do let __do_lift ← Auto.LamReif.getRst pure __do_lift.maxEVarSucc

def Auto.LamReif.getLamEVarTy : ReifM (Array Embedding.Lam.LamSort)

Equations

• Auto.LamReif.getLamEVarTy = do let __do_lift ← Auto.LamReif.getRst pure __do_lift.lamEVarTy

def Auto.LamReif.getLamEVarTyTree : ReifM (BinTree Embedding.Lam.LamSort)

Equations

• Auto.LamReif.getLamEVarTyTree = do let __do_lift ← Auto.LamReif.getRst pure __do_lift.lamEVarTyTree

def Auto.LamReif.getChkMap : ReifM (Std.HashMap Embedding.Lam.REntry Embedding.Lam.ChkStep)

Equations

• Auto.LamReif.getChkMap = do let __do_lift ← Auto.LamReif.getRst pure __do_lift.chkMap

def Auto.LamReif.checkerStats : ReifM (Array (String × Nat))

Equations

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

def Auto.LamReif.printCheckerStats : ReifM Unit

Equations

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

def Auto.LamReif.printValuation : ReifM Unit

Equations

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

def Auto.LamReif.printProofs : ReifM Unit

Equations

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

def Auto.LamReif.sort2LamILTyIdx (s : Embedding.Lam.LamSort) : ReifM Nat

Equations

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

def Auto.LamReif.lookupTyVal! (n : Nat) : ReifM (Lean.Expr × Lean.Level)

Equations

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

def Auto.LamReif.lookupVarVal! (n : Nat) : ReifM (Lean.Expr × Embedding.Lam.LamSort)

Lookup valuation of term atom

Equations

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

def Auto.LamReif.lookupLamILTy! (idx : Nat) : ReifM Embedding.Lam.LamSort

Equations

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

def Auto.LamReif.lookupAssertion! (t : Embedding.Lam.LamTerm) : ReifM (Lean.Expr × DTr × Embedding.Lam.LamTerm × Nat)

Equations

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

def Auto.LamReif.lookupRTable! (pos : Nat) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.lookupREntryPos! (re : Embedding.Lam.REntry) : ReifM Nat

Equations

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

inductive Auto.LamReif.REntryProof : Type

• chkStep : Embedding.Lam.ChkStep → REntryProof
• inhabitation : Lean.Expr → DTr → Embedding.Lam.LamSort → REntryProof
• assertion : Lean.Expr → DTr → Embedding.Lam.LamTerm → REntryProof

def Auto.LamReif.lookupREntryProof? (re : Embedding.Lam.REntry) : ReifM (Option REntryProof)

Equations

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

def Auto.LamReif.lookupREntryProof! (re : Embedding.Lam.REntry) : ReifM REntryProof

Equations

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

def Auto.LamReif.lookupLamEVarTy! (idx : Nat) : ReifM Embedding.Lam.LamSort

Equations

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

def Auto.LamReif.lookupChkStepEtom! (cs : Embedding.Lam.ChkStep) : ReifM (Array Nat)

Equations

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

def Auto.LamReif.lookupChkStepResult! (cs : Embedding.Lam.ChkStep) : ReifM Embedding.Lam.EvalResult

Equations

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

def Auto.LamReif.lookupEtomChkStep! (eidx : Nat) : ReifM Embedding.Lam.ChkStep

Equations

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

def Auto.LamReif.getLamTyValAtMeta : ReifM Embedding.Lam.LamTyVal

This should only be used at the meta level, i.e. in code that will be evaluated during the execution of auto

Equations

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

def Auto.LamReif.resolveLamBaseTermImport : Embedding.Lam.LamBaseTerm → ReifM Embedding.Lam.LamBaseTerm

Equations

• Auto.LamReif.resolveLamBaseTermImport (Auto.Embedding.Lam.LamBaseTerm.eqI n) = do let __do_lift ← Auto.LamReif.lookupLamILTy! n pure (Auto.Embedding.Lam.LamBaseTerm.eq __do_lift)
• Auto.LamReif.resolveLamBaseTermImport (Auto.Embedding.Lam.LamBaseTerm.forallEI n) = do let __do_lift ← Auto.LamReif.lookupLamILTy! n pure (Auto.Embedding.Lam.LamBaseTerm.forallE __do_lift)
• Auto.LamReif.resolveLamBaseTermImport (Auto.Embedding.Lam.LamBaseTerm.existEI n) = do let __do_lift ← Auto.LamReif.lookupLamILTy! n pure (Auto.Embedding.Lam.LamBaseTerm.existE __do_lift)
• Auto.LamReif.resolveLamBaseTermImport (Auto.Embedding.Lam.LamBaseTerm.iteI n) = do let __do_lift ← Auto.LamReif.lookupLamILTy! n pure (Auto.Embedding.Lam.LamBaseTerm.ite __do_lift)
• Auto.LamReif.resolveLamBaseTermImport x✝ = pure x✝

def Auto.LamReif.resolveImport : Embedding.Lam.LamTerm → ReifM Embedding.Lam.LamTerm

Models resolveImport on the meta level

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.resolveImport (Auto.Embedding.Lam.LamTerm.atom n) = pure (Auto.Embedding.Lam.LamTerm.atom n)
• Auto.LamReif.resolveImport (Auto.Embedding.Lam.LamTerm.etom a) = Lean.throwError (Lean.toMessageData `Auto.LamReif.resolveImport ++ Lean.toMessageData " :: etom should not occur here")
• Auto.LamReif.resolveImport (Auto.Embedding.Lam.LamTerm.base b) = do let __do_lift ← Auto.LamReif.resolveLamBaseTermImport b pure (Auto.Embedding.Lam.LamTerm.base __do_lift)
• Auto.LamReif.resolveImport (Auto.Embedding.Lam.LamTerm.bvar n) = pure (Auto.Embedding.Lam.LamTerm.bvar n)
• Auto.LamReif.resolveImport (Auto.Embedding.Lam.LamTerm.lam s t) = do let __do_lift ← Auto.LamReif.resolveImport t pure (Auto.Embedding.Lam.LamTerm.lam s __do_lift)

def Auto.LamReif.mkImportVersion : Embedding.Lam.LamTerm → ReifM Embedding.Lam.LamTerm

This is the inverse of resolveImport · When importing external proof H : α, we will reify α into t : LamTerm using reifTerm. The t returned by reifTerm has eq for Eq, forallE for ∀, existE for ∃ and ite for Auto.Bool.ite' · It's easy to see that t.interp will not be definitionally equal to α because =, ∀, ∃, ite' within α operates on the original domain, while =, ∀, ∃, ite' in t.interp operates on the lifted domain · Therefore, we need to turn =, ∀, ∃, ite' in t into import version to get t', and design an appropriate ilVal, such that GLift.down t'.interp is definitionally equal to α

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.mkImportVersion (Auto.Embedding.Lam.LamTerm.atom n) = pure (Auto.Embedding.Lam.LamTerm.atom n)
• Auto.LamReif.mkImportVersion (Auto.Embedding.Lam.LamTerm.etom a) = Lean.throwError (Lean.toMessageData `Auto.LamReif.mkImportVersion ++ Lean.toMessageData " :: etom should not occur here")
• Auto.LamReif.mkImportVersion (Auto.Embedding.Lam.LamTerm.base b) = pure (Auto.Embedding.Lam.LamTerm.base b)
• Auto.LamReif.mkImportVersion (Auto.Embedding.Lam.LamTerm.bvar n) = pure (Auto.Embedding.Lam.LamTerm.bvar n)
• Auto.LamReif.mkImportVersion (Auto.Embedding.Lam.LamTerm.lam s t) = do let __do_lift ← Auto.LamReif.mkImportVersion t pure (Auto.Embedding.Lam.LamTerm.lam s __do_lift)

def Auto.LamReif.newChkStep (c : Embedding.Lam.ChkStep) (res? : Option Embedding.Lam.EvalResult) : ReifM (Bool × Embedding.Lam.EvalResult)

A new ChkStep. res is the expected result of the ChkStep Returns:

1. Whether the checkstep produces a new REntry
2. The EvalResult of this checkstep

Equations

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

def Auto.LamReif.addREntryToRTable (re : Embedding.Lam.REntry) : ReifM Nat

Returns the position of the entry inside the RTable

Equations

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

def Auto.LamReif.newAssertion (proof : Lean.Expr) (deriv : DTr) (ty : Embedding.Lam.LamTerm) : ReifM Unit

ty is a reified assumption. ∀, ∃ and = in ty are supposed to not be of the import version The type of proof is definitionally equal to GLift.down (← mkImportVersion ty).interp Returns the position of ty inside the validTable after inserting it

Equations

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

def Auto.LamReif.inhSubsumptionCheck (s : Embedding.Lam.LamSort) : ReifM Bool

Returns false if s is subsumed by previous inhabited sorts Returns true if not

Equations

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

def Auto.LamReif.newInhabitation (inh : Lean.Expr) (deriv : DTr) (s : Embedding.Lam.LamSort) : ReifM Unit

The type of inh should be definitionally equal to s.interpAsUnlifted

Equations

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

partial def Auto.LamReif.updownFunc (s : Embedding.Lam.LamSort) : ReifM (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

def Auto.LamReif.varValInterp (e : Lean.Expr) (s : Embedding.Lam.LamSort) : ReifM Lean.Expr

(e, s) is a pair from the varVal field of LamReif.ReifM.State Returns the lifted counterpart of e

Equations

• Auto.LamReif.varValInterp e s = do let __discr ← Auto.LamReif.updownFunc s match __discr with | (up, fst, fst_1, snd) => pure (up.app e)

def Auto.LamReif.mkIsomType (upFunc downFunc ty upTy : Lean.Expr) (uOrig : Lean.Level) : ReifM Lean.Expr

Equations

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

def Auto.LamReif.mkImportingILLift (s : Embedding.Lam.LamSort) : ReifM Lean.Expr

Suppose u ← getU, this function returns a term of type ILLift.{u} s.interpAsLifted

Equations

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

def Auto.LamReif.nonemptyOfAtom (n : Nat) : ReifM (Option Embedding.Lam.REntry)

Equations

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

def Auto.LamReif.nonemptyOfEtom (n : Nat) : ReifM (Option Embedding.Lam.REntry)

Equations

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

def Auto.LamReif.validOfIntros (v : Embedding.Lam.REntry) (idx : Nat) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfIntroMost (v : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.validOfIntroMost v = Lean.throwError (Lean.toMessageData `Auto.LamReif.validOfIntroMost ++ Lean.toMessageData " :: Unexpected entry " ++ Lean.toMessageData v)

def Auto.LamReif.validOfReverts (v : Embedding.Lam.REntry) (idx : Nat) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfRevertAll (v : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.validOfRevertAll v = Lean.throwError (Lean.toMessageData `Auto.LamReif.validOfRevertAll ++ Lean.toMessageData " :: Unexpected entry " ++ Lean.toMessageData v)

def Auto.LamReif.validOfAppend (v : Embedding.Lam.REntry) (ex : Array Embedding.Lam.LamSort) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfPrepend (v : Embedding.Lam.REntry) (ex : Array Embedding.Lam.LamSort) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfHeadBeta (v : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfHnf (v : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfBetaBounded (v : Embedding.Lam.REntry) (bound : Nat) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfBetaReduce (v : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

• Auto.LamReif.validOfBetaReduce (Auto.Embedding.Lam.REntry.valid a t) = Auto.LamReif.validOfBetaBounded (Auto.Embedding.Lam.REntry.valid a t) t.betaReduceHackyIdx
• Auto.LamReif.validOfBetaReduce v = Lean.throwError (Lean.toMessageData `Auto.LamReif.validOfBetaReduce ++ Lean.toMessageData " :: Unexpected entry " ++ Lean.toMessageData v)

def Auto.LamReif.validOfExtensionalize (v : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfEqSymm (v : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfMp (vp vrw : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfMpAll (vp vrw : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfEtaExpand1At (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfEtaReduce1At (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfEtaExpandNAt (v : Embedding.Lam.REntry) (n : Nat) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfEtaReduceNAt (v : Embedding.Lam.REntry) (n : Nat) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfEtaExpandAt (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.validOfEtaExpandAt v occ = Lean.throwError (Lean.toMessageData `Auto.LamReif.validOfEtaExpandAt ++ Lean.toMessageData " :: Unexpected entry " ++ Lean.toMessageData v)

def Auto.LamReif.validOfEtaReduceAt (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.validOfEtaReduceAt v occ = Lean.throwError (Lean.toMessageData `Auto.LamReif.validOfEtaReduceAt ++ Lean.toMessageData " :: Unexpected entry " ++ Lean.toMessageData v)

def Auto.LamReif.validOfExtensionalizeEqAt (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfExtensionalizeEqFNAt (v : Embedding.Lam.REntry) (n : Nat) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfIntensionalizeEqAt (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfBVarLower (v n : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfBVarLowers (v : Embedding.Lam.REntry) (ns : Array Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfElimForalls (v : Embedding.Lam.REntry) (ns : Array Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Given ∀ (_ : s₀) (_ : s₁) ⋯ (_ : sₖ₋₁), body and the fact that s₀, s₁, ⋯, sₖ₋₁ are nonempty, return a proof of body

Equations

• Auto.LamReif.validOfElimForalls v ns = do let introed ← Auto.LamReif.validOfIntros v ns.size Auto.LamReif.validOfBVarLowers introed ns.reverse

def Auto.LamReif.validOfImp (v₁₂ v₁ : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfImps (impV : Embedding.Lam.REntry) (hypVs : Array Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfInstantiate (v : Embedding.Lam.REntry) (args : Array Embedding.Lam.LamTerm) : ReifM Embedding.Lam.REntry

Repeated instantiation

Equations

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

def Auto.LamReif.validOfInstantiateRev (v : Embedding.Lam.REntry) (args : Array Embedding.Lam.LamTerm) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfInstantiateForall (v : Embedding.Lam.REntry) (args : Array Embedding.Lam.LamTerm) : ReifM Embedding.Lam.REntry

Given ∀ x₀ x₁ ⋯ xₖ₋₁, p and arg₀, arg₁, ⋯, argₖ₋₁, return p[x₀/arg₀, x₁/arg₁, ⋯, xₖ₋₁/argₖ₋₁]

Equations

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

def Auto.LamReif.validOfAndLeft (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfAndRight (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

partial def Auto.LamReif.decomposeAnd (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM (Array Embedding.Lam.REntry)

Exhaustively decompose ∧ at position occ

def Auto.LamReif.boolFacts : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.iteSpec (s : Embedding.Lam.LamSort) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.skolemize (exV : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.skolemizeMostIntoForall (exV : Embedding.Lam.REntry) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.define (t : Embedding.Lam.LamTerm) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.validOfPrepConv (pc : Embedding.Lam.PrepConvStep) (v : Embedding.Lam.REntry) (occ : List Bool) : ReifM Embedding.Lam.REntry

Equations

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

def Auto.LamReif.reorderLCtx (v : Embedding.Lam.REntry) (rmap : Array Nat) : ReifM Embedding.Lam.REntry

.bvar i will be turned into .bvar map[i] It is required that the size of rmap is equal to the length of local context

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.reorderLCtx v rmap = Lean.throwError (Lean.toMessageData `Auto.LamReif.reorderLCtx ++ Lean.toMessageData " :: Unexpected entry " ++ Lean.toMessageData v)

def Auto.LamReif.toDefinition? (v : Embedding.Lam.REntry) : ReifM (Option Embedding.Lam.REntry)

Refer to docstring of LamTerm.isGeneral

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.toDefinition? v = Lean.throwError (Lean.toMessageData `Auto.LamReif.toDefinition? ++ Lean.toMessageData " :: Unexpected entry " ++ Lean.toMessageData v)

def Auto.LamReif.recognizeDefsAndUnfold (vs : Array Embedding.Lam.REntry) (minds : Array Embedding.Lam.MutualIndInfo) : ReifM (Array Embedding.Lam.REntry × Array Embedding.Lam.MutualIndInfo)

Recognize all definitions-like facts within vs, exhaustively rewrite using them and remove them in the end Meanwhile, all λterms in the ts are rewritten using the recognied definitions

Equations

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

opaque Auto.LamReif.auto.lamReif.prep.def : Lean.Option Bool

def Auto.LamReif.preprocess (vs : Array Embedding.Lam.REntry) (minds : Array Embedding.Lam.MutualIndInfo) : ReifM (Array Embedding.Lam.REntry × Array Embedding.Lam.MutualIndInfo)

Equations

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

def Auto.LamReif.auxLemmas (vs : Array Embedding.Lam.REntry) : ReifM (Array Embedding.Lam.REntry)

Equations

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

def Auto.LamReif.newTermExprAux (e : Lean.Expr) (sort : Embedding.Lam.LamSort) : ReifM Embedding.Lam.LamTerm

Accept a new expression representing λterm atom Returns the index of it in the varVal array

Equations

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

def Auto.LamReif.newTypeExpr (e : Lean.Expr) : ReifM Embedding.Lam.LamSort

Equations

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

def Auto.LamReif.processTypeExpr (e : Lean.Expr) : ReifM Embedding.Lam.LamSort

Equations

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

def Auto.LamReif.reifType (e : Lean.Expr) : ReifM Embedding.Lam.LamSort

Equations

• Auto.LamReif.reifType e = do let e ← liftM (Auto.prepReduceTypeForall e) Auto.LamReif.reifTypeAux✝ e

def Auto.LamReif.newTermExpr (e : Lean.Expr) : ReifM Embedding.Lam.LamTerm

Equations

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

def Auto.LamReif.reifMapIL : Std.HashMap Lean.Name (Embedding.Lam.LamSort → Embedding.Lam.LamBaseTerm)

Equations

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

def Auto.LamReif.reifMapConstNilLvl : Std.HashMap Lean.Name Embedding.Lam.LamTerm

Equations

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

def Auto.LamReif.reifMapBVConst1 : Std.HashMap Lean.Name (Nat → Embedding.Lam.LamTerm)

Equations

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

def Auto.LamReif.reifMapBVConst2 : Std.HashMap Lean.Name (Nat → Nat → Embedding.Lam.LamTerm)

Equations

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

def Auto.LamReif.reifMapBVConst3 : Std.HashMap Lean.Name (Nat → Nat → Nat → Embedding.Lam.LamTerm)

Equations

• Auto.LamReif.reifMapBVConst3 = Std.HashMap.ofList [(`BitVec.extractLsb, fun (n h l : Nat) => Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.bvextract n h l))]

def Auto.LamReif.reifMapAttributesProp : Std.HashMap Lean.Name String

Equations

• Auto.LamReif.reifMapAttributesProp = Std.HashMap.ofList [(`Auto.SMT.Attribute.trigger, "pattern")]

def Auto.LamReif.processSimpleLit (l : Lean.Literal) : Embedding.Lam.LamTerm

Equations

• Auto.LamReif.processSimpleLit (Lean.Literal.natVal n) = Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.natVal n)
• Auto.LamReif.processSimpleLit (Lean.Literal.strVal s) = Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.strVal s)

def Auto.LamReif.processSimpleConst (name : Lean.Name) (lvls : List Lean.Level) : ReifM (Option Embedding.Lam.LamTerm)

Equations

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

def Auto.LamReif.processSimpleApp (fn arg : Lean.Expr) : ReifM (Option Embedding.Lam.LamTerm)

Equations

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

def Auto.LamReif.reifMapLam0Arg2NoLit : Std.HashMap (Lean.Name × Lean.Name) (Lean.Expr × Embedding.Lam.LamTerm)

fn : .const _ _ arg₁ : .const _ _

Equations

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

def Auto.LamReif.reifMapLam0Arg2Natlit : Std.HashMap (Lean.Name × Lean.Name) (Array ((Nat → Lean.Expr) × (Nat → Embedding.Lam.LamTerm)))

fn : .const _ _ arg₁ : .app (.const _ _) natlit

Equations

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

def Auto.LamReif.reifMapLam0Arg4NoLit : Std.HashMap (Lean.Name × Lean.Name × Lean.Name) (Lean.Expr × Embedding.Lam.LamTerm)

fn : .const _ _ arg₁ : .const _ _ arg₂ : .const _ _

Equations

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

def Auto.LamReif.reifMapLam0Arg4NatLitNatLitEq : Std.HashMap (Lean.Name × Lean.Name) (Array ((Nat → Lean.Expr) × (Nat → Embedding.Lam.LamTerm)))

fn : .const _ _ arg₁ : .app (.const _ _) natlit₁ arg₂ : .app (.const _ _) natlit₂ |- natlit₁ = natlit₂

Equations

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

def Auto.LamReif.reifMapLam0Arg4NatLitNatLitH : Std.HashMap (Lean.Name × Lean.Name) (Array ((Nat → Nat → Lean.Expr) × (Nat → Nat → Embedding.Lam.LamTerm)))

fn : .const _ _ arg₁ : .app (.const _ _) natlit₁ arg₂ : .app (.const _ _) natlit₂ |- natlit₁ ?? natlit₂

Equations

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

def Auto.LamReif.reifMapLam0Arg4NatLit : Std.HashMap (Lean.Name × Lean.Name) (Array ((Nat → Lean.Expr) × (Nat → Embedding.Lam.LamTerm)))

fn : .const _ _ arg₁ : .app (.const _ _) natlit arg₂ : .const _ _

Equations

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

def Auto.LamReif.processLam0Arg2 (e fn arg₁ _arg₂ : Lean.Expr) : Lean.MetaM (Option Embedding.Lam.LamTerm)

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.processLam0Arg2 e fn arg₁ _arg₂ = pure none

def Auto.LamReif.processLam0Arg3 (e fn arg₁ arg₂ _arg₃ : Lean.Expr) : Lean.MetaM (Option Embedding.Lam.LamTerm)

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.processLam0Arg3 e (Lean.Expr.const `OfNat.ofNat us) arg₁ arg₂ _arg₃ = pure none
• Auto.LamReif.processLam0Arg3 e fn arg₁ arg₂ _arg₃ = pure none

def Auto.LamReif.processLam0Arg4 (e fn arg₁ arg₂ _arg₃ _arg₄ : Lean.Expr) : Lean.MetaM (Option Embedding.Lam.LamTerm)

Equations

• One or more equations did not get rendered due to their size.
• Auto.LamReif.processLam0Arg4 e fn arg₁ arg₂ _arg₃ _arg₄ = pure none

def Auto.LamReif.processComplexTermExpr (e : Lean.Expr) : Lean.MetaM (Option Embedding.Lam.LamTerm)

Equations

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

def Auto.LamReif.processNewTermExpr (e : Lean.Expr) : ReifM Embedding.Lam.LamTerm

Equations

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

def Auto.LamReif.processNewTermExpr.processOther (e : Lean.Expr) : ReifM Embedding.Lam.LamTerm

Equations

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

def Auto.LamReif.processTermExpr (lctx : Std.HashMap Lean.FVarId Nat) (e : Lean.Expr) : ReifM Embedding.Lam.LamTerm

Equations

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

def Auto.LamReif.processTermExpr.deBruijn? (lctx : Std.HashMap Lean.FVarId Nat) (id : Lean.FVarId) : Option Nat

Equations

• Auto.LamReif.processTermExpr.deBruijn? lctx id = match lctx.get? id with | some n => some (lctx.size - 1 - n) | none => none

partial def Auto.LamReif.reifTerm (lctx : Std.HashMap Lean.FVarId Nat) : Lean.Expr → ReifM Embedding.Lam.LamTerm

def Auto.LamReif.reifTermCheckType (e : Lean.Expr) : ReifM (Embedding.Lam.LamSort × Embedding.Lam.LamTerm)

Equations

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

def Auto.LamReif.reifFacts (facts : Array UMonoFact) : ReifM (Array Embedding.Lam.LamTerm)

Return the positions of the reified and resolveImport-ed facts within the validTable

Equations

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

def Auto.LamReif.reifInhabitations (inhs : Array UMonoFact) : ReifM (Array Embedding.Lam.LamSort)

Equations

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

def Auto.LamReif.reifInd (ind : SimpleIndVal) : ReifM (Option Embedding.Lam.IndInfo)

Equations

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

def Auto.LamReif.reifMutInd (mind : Array SimpleIndVal) : ReifM (Option Embedding.Lam.MutualIndInfo)

Equations

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

def Auto.LamReif.reifMutInds (minds : Array (Array SimpleIndVal)) : ReifM (Array Embedding.Lam.MutualIndInfo)

Equations

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

partial def Auto.LamReif.collectDerivFor (re : Embedding.Lam.REntry) : ReifM DTr

inductive Auto.LamReif.BuildMode : Type

• directReduce : BuildMode
• indirectReduce : BuildMode
• indirectReduce_reflection : BuildMode

instance Auto.LamReif.instBEqBuildMode : BEq BuildMode

Equations

• Auto.LamReif.instBEqBuildMode = { beq := Auto.LamReif.instBEqBuildMode.beq }

def Auto.LamReif.instBEqBuildMode.beq : BuildMode → BuildMode → Bool

Equations

• Auto.LamReif.instBEqBuildMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Auto.LamReif.instHashableBuildMode.hash : BuildMode → UInt64

Equations

• Auto.LamReif.instHashableBuildMode.hash Auto.LamReif.BuildMode.directReduce = 0
• Auto.LamReif.instHashableBuildMode.hash Auto.LamReif.BuildMode.indirectReduce = 1
• Auto.LamReif.instHashableBuildMode.hash Auto.LamReif.BuildMode.indirectReduce_reflection = 2

instance Auto.LamReif.instHashableBuildMode : Hashable BuildMode

Equations

• Auto.LamReif.instHashableBuildMode = { hash := Auto.LamReif.instHashableBuildMode.hash }

instance Auto.LamReif.instInhabitedBuildMode : Inhabited BuildMode

Equations

• Auto.LamReif.instInhabitedBuildMode = { default := Auto.LamReif.instInhabitedBuildMode.default }

def Auto.LamReif.instInhabitedBuildMode.default : BuildMode

Equations

• Auto.LamReif.instInhabitedBuildMode.default = Auto.LamReif.BuildMode.directReduce

instance Auto.LamReif.instToStringBuildMode : ToString BuildMode

Equations

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

instance Auto.LamReif.instValueBuildMode : Lean.KVMap.Value BuildMode

Equations

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

opaque Auto.LamReif.auto.checker.buildMode : Lean.Option BuildMode

def Auto.LamReif.buildChkStepsExpr : ReifM Lean.Expr

Equations

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

def Auto.LamReif.buildTyVal : ReifM Lean.Expr

Equations

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

def Auto.LamReif.buildVarExpr (tyValExpr : Lean.Expr) : ReifM Lean.Expr

Build LamVarTy and varVal

Equations

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

def Auto.LamReif.buildILExpr (tyValExpr : Lean.Expr) : ReifM Lean.Expr

Build lamILTy and ilVal

Equations

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

def Auto.LamReif.buildCPValExpr : ReifM Lean.Expr

Equations

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

def Auto.LamReif.buildImportTableExpr (chkValExpr : Lean.Expr) : ReifM (Lean.Expr × Lean.Expr)

lvalExpr is the LamValuation

Equations

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

def Auto.LamReif.buildFullCheckerExprFor_directReduce (re : Embedding.Lam.REntry) : ReifM Lean.Expr

re is the entry we want to retrieve from the validTable The expr returned is a proof of the LamThmValid-ness of the entry

Equations

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

def Auto.LamReif.buildFullCheckerExprFor_indirectReduce (re : Embedding.Lam.REntry) : ReifM Lean.Expr

re is the entry we want to retrieve from the validTable The expr returned is a proof of the LamThmValid-ness of the entry

Equations

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

def Auto.LamReif.compileRunResultExpr : ReifM Lean.Name

This can be used to shows the issue that compilation of a reduced expression exhibits superlinear behaviour. Try the examples in Test/CheckerScalability/Skolemization.lean This function is not intended to be called in practice

Equations

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

def Auto.LamReif.buildFullCheckerExprFor_indirectReduce_reflection (re : Embedding.Lam.REntry) : ReifM Lean.Expr

Equations

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

def Auto.LamReif.buildFullCheckerExprFor (re : Embedding.Lam.REntry) : ReifM Lean.Expr

Equations

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

structure Auto.Lam2Lam.TState : Type

• typeH2lMap : Std.HashMap Nat Nat
• typeL2hMap : Array Nat
• termH2lMap : Std.HashMap Nat Nat
• termL2hMap : Array Nat
• etomH2lMap : Std.HashMap Nat Nat
• etomL2hMap : Std.HashMap Nat Nat
• csH2lMap : Std.HashMap Embedding.Lam.ChkStep Embedding.Lam.ChkStep

@[reducible, inline]

abbrev Auto.Lam2Lam.TransM (α : Type) : Type

Equations

• Auto.Lam2Lam.TransM = StateRefT' IO.RealWorld Auto.Lam2Lam.TState Auto.LamReif.ReifM

@[always_inline]

instance Auto.Lam2Lam.instMonadTransM : Monad TransM

Equations

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

instance Auto.Lam2Lam.instInhabitedTransM {α : Type} : Inhabited (TransM α)

Equations

• Auto.Lam2Lam.instInhabitedTransM = { default := fun (x : ST.Ref IO.RealWorld Auto.Lam2Lam.TState) => throw default }

def Auto.Lam2Lam.getTermL2hMap : TransM (Array Nat)

Equations

• Auto.Lam2Lam.getTermL2hMap = do let st ← get pure st.termL2hMap

def Auto.Lam2Lam.setTypeL2hMap (field : Array Nat) : TransM PUnit

Equations

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

def Auto.Lam2Lam.setCsH2lMap (field : Std.HashMap Embedding.Lam.ChkStep Embedding.Lam.ChkStep) : TransM PUnit

Equations

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

def Auto.Lam2Lam.setTermL2hMap (field : Array Nat) : TransM PUnit

Equations

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

def Auto.Lam2Lam.getCsH2lMap : TransM (Std.HashMap Embedding.Lam.ChkStep Embedding.Lam.ChkStep)

Equations

• Auto.Lam2Lam.getCsH2lMap = do let st ← get pure st.csH2lMap

def Auto.Lam2Lam.getEtomH2lMap : TransM (Std.HashMap Nat Nat)

Equations

• Auto.Lam2Lam.getEtomH2lMap = do let st ← get pure st.etomH2lMap

def Auto.Lam2Lam.getTermH2lMap : TransM (Std.HashMap Nat Nat)

Equations

• Auto.Lam2Lam.getTermH2lMap = do let st ← get pure st.termH2lMap

def Auto.Lam2Lam.getTypeH2lMap : TransM (Std.HashMap Nat Nat)

Equations

• Auto.Lam2Lam.getTypeH2lMap = do let st ← get pure st.typeH2lMap

def Auto.Lam2Lam.setEtomH2lMap (field : Std.HashMap Nat Nat) : TransM PUnit

Equations

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

def Auto.Lam2Lam.getTypeL2hMap : TransM (Array Nat)

Equations

• Auto.Lam2Lam.getTypeL2hMap = do let st ← get pure st.typeL2hMap

def Auto.Lam2Lam.setTypeH2lMap (field : Std.HashMap Nat Nat) : TransM PUnit

Equations

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

def Auto.Lam2Lam.getEtomL2hMap : TransM (Std.HashMap Nat Nat)

Equations

• Auto.Lam2Lam.getEtomL2hMap = do let st ← get pure st.etomL2hMap

def Auto.Lam2Lam.setEtomL2hMap (field : Std.HashMap Nat Nat) : TransM PUnit

Equations

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

def Auto.Lam2Lam.setTermH2lMap (field : Std.HashMap Nat Nat) : TransM PUnit

Equations

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

def Auto.Lam2Lam.transTypeAtom (a : Nat) (val : Lean.Expr × Lean.Level) : TransM Nat

Equations

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

def Auto.Lam2Lam.transTermAtom (a : Nat) (val : Lean.Expr × Embedding.Lam.LamSort) : TransM Nat

When translating Lam to Lam in Lam2Lam, make sure that the LamSort in this val is already translated.

Equations

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

def Auto.Lam2Lam.addEtomTranslation (eH eL : Nat) : TransM Unit

Equations

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

def Auto.Lam2Lam.transLamSort (ref : LamReif.State) : Embedding.Lam.LamSort → TransM Embedding.Lam.LamSort

Equations

• One or more equations did not get rendered due to their size.
• Auto.Lam2Lam.transLamSort ref (Auto.Embedding.Lam.LamSort.base b) = pure (Auto.Embedding.Lam.LamSort.base b)
• Auto.Lam2Lam.transLamSort ref (s₁.func s₂) = Auto.Embedding.Lam.LamSort.func <$> Auto.Lam2Lam.transLamSort ref s₁ <*> Auto.Lam2Lam.transLamSort ref s₂

def Auto.Lam2Lam.transLamBaseTerm (ref : LamReif.State) : Embedding.Lam.LamBaseTerm → TransM Embedding.Lam.LamBaseTerm

Equations

• Auto.Lam2Lam.transLamBaseTerm ref (Auto.Embedding.Lam.LamBaseTerm.eqI a) = Lean.throwError ((Lean.MessageData.ofFormat ∘ Std.format) Auto.Lam2Lam.transLamBaseTermILErr✝)
• Auto.Lam2Lam.transLamBaseTerm ref (Auto.Embedding.Lam.LamBaseTerm.forallEI a) = Lean.throwError ((Lean.MessageData.ofFormat ∘ Std.format) Auto.Lam2Lam.transLamBaseTermILErr✝)
• Auto.Lam2Lam.transLamBaseTerm ref (Auto.Embedding.Lam.LamBaseTerm.existEI a) = Lean.throwError ((Lean.MessageData.ofFormat ∘ Std.format) Auto.Lam2Lam.transLamBaseTermILErr✝)
• Auto.Lam2Lam.transLamBaseTerm ref (Auto.Embedding.Lam.LamBaseTerm.iteI a) = Lean.throwError ((Lean.MessageData.ofFormat ∘ Std.format) Auto.Lam2Lam.transLamBaseTermILErr✝)
• Auto.Lam2Lam.transLamBaseTerm ref (Auto.Embedding.Lam.LamBaseTerm.eq s) = Auto.Embedding.Lam.LamBaseTerm.eq <$> Auto.Lam2Lam.transLamSort ref s
• Auto.Lam2Lam.transLamBaseTerm ref (Auto.Embedding.Lam.LamBaseTerm.forallE s) = Auto.Embedding.Lam.LamBaseTerm.forallE <$> Auto.Lam2Lam.transLamSort ref s
• Auto.Lam2Lam.transLamBaseTerm ref (Auto.Embedding.Lam.LamBaseTerm.existE s) = Auto.Embedding.Lam.LamBaseTerm.existE <$> Auto.Lam2Lam.transLamSort ref s
• Auto.Lam2Lam.transLamBaseTerm ref (Auto.Embedding.Lam.LamBaseTerm.ite s) = Auto.Embedding.Lam.LamBaseTerm.ite <$> Auto.Lam2Lam.transLamSort ref s
• Auto.Lam2Lam.transLamBaseTerm ref x✝ = pure x✝

partial def Auto.Lam2Lam.transEtom (ref : LamReif.State) (e : Nat) : TransM Nat

partial def Auto.Lam2Lam.transLamTerm (ref : LamReif.State) : Embedding.Lam.LamTerm → TransM Embedding.Lam.LamTerm

partial def Auto.Lam2Lam.transREntry (ref : LamReif.State) : Embedding.Lam.REntry → TransM Embedding.Lam.REntry

partial def Auto.Lam2Lam.transPos (ref : LamReif.State) (n : Nat) : TransM Nat

partial def Auto.Lam2Lam.transChkStep (ref : LamReif.State) : Embedding.Lam.ChkStep → TransM Embedding.Lam.ChkStep

partial def Auto.Lam2Lam.processChkStep (ref : LamReif.State) (cs : Embedding.Lam.ChkStep) : TransM Embedding.Lam.EvalResult

partial def Auto.Lam2Lam.collectProofFor (ref : LamReif.State) (hre : Embedding.Lam.REntry) : TransM Unit

def Auto.Lam2Lam.optimizedStateFor (res : Array Embedding.Lam.REntry) : LamReif.ReifM LamReif.State

Delete irrelevant Valuations and ChkSteps, but make sure that entries in res are still provable

Equations

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

def Auto.LamReif.buildOptimizedCheckerExprFor (re : Embedding.Lam.REntry) : ReifM Lean.Expr

Build optimized checker = Optimize state + Build full checker

Equations

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

opaque Auto.LamReif.auto.optimizeCheckerProof : Lean.Option Bool

def Auto.LamReif.buildCheckerExprFor (re : Embedding.Lam.REntry) : ReifM Lean.Expr

Decide whether to optimize based on option

Equations

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