def getClauseInfo! (state : Duper.ProverM.State) (c : Duper.Clause) : Lean.CoreM Duper.ProverM.ClauseInfo

Equations

• getClauseInfo! state c = match state.allClauses.get? c with | some ci => pure ci | x => Lean.throwError (Lean.toMessageData "clause info not found: " ++ Lean.toMessageData c)

def printProof (state : Duper.ProverM.State) : Lean.MetaM Unit

Equations

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

partial def printProof.go (state : Duper.ProverM.State) (c : Duper.Clause) (hm : Array (Nat × Duper.Clause) := ∅) : Lean.MetaM (Array (Nat × Duper.Clause))

@[reducible, inline]

abbrev ClauseHeap : Type

Equations

• ClauseHeap = Batteries.BinomialHeap (Nat × Duper.Clause) fun (c d : Nat × Duper.Clause) => decide (c.fst ≤ d.fst)

partial def collectClauses (state : Duper.ProverM.State) (c : Duper.Clause) (acc : Array Nat × ClauseHeap) : Lean.MetaM (Array Nat × ClauseHeap)

@[reducible, inline]

abbrev LevelRequests : Type

Equations

• LevelRequests = Std.HashMap Nat (Std.HashMap (Array Lean.Level) Nat)

partial def collectLevelRequests (state : Duper.ProverM.State) (c : Duper.Clause) (lvls : Array Lean.Level) (acc : LevelRequests) : Lean.MetaM LevelRequests

structure PRContext : Type

• pmstate : Duper.ProverM.State
• reqs : LevelRequests

structure PRState : Type

• constructedClauses : Std.HashMap (Nat × Array Lean.Level) Lean.Expr
• constructedSkolems : Std.HashMap Nat Lean.FVarId
• lctx : Lean.LocalContext
• mctx : Lean.MetavarContext
• localInstances : Lean.LocalInstances
• fvars : Array Lean.Expr

instance instInhabitedPRState : Inhabited PRState

Equations

• instInhabitedPRState = { default := instInhabitedPRState.default }

def instInhabitedPRState.default : PRState

Equations

• instInhabitedPRState.default = { constructedClauses := default, constructedSkolems := default, lctx := default, mctx := default, localInstances := default, fvars := default }

def PRState.insertConstructedClauses (prs : PRState) (key : Nat × Array Lean.Level) (val : Lean.Expr) : PRState

Equations

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

@[reducible, inline]

abbrev PRM (α : Type) : Type

Equations

• PRM = ReaderT PRContext (StateRefT' IO.RealWorld PRState Lean.CoreM)

def PRM.mkLetDecl (fvarId : Lean.FVarId) (userName : Lean.Name) (type value : Lean.Expr) (nonDep : Bool := false) (kind : Lean.LocalDeclKind := default) : PRM Unit

Equations

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

def runMetaAsPRM {α : Type} (x : Lean.MetaM α) : PRM α

Equations

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

def PRM.run {α : Type} (m : PRM α) (ctx : PRContext) (st : PRState) : Lean.CoreM (α × PRState)

Equations

• m.run ctx st = (m ctx).run st

partial def PRM.matchSkolem : Lean.Expr → PRM Lean.TransformStep

partial def mkClauseProof : List Duper.Clause → PRM Lean.Expr

def mkAllProof (state : Duper.ProverM.State) (cs : List Duper.Clause) : Lean.MetaM Lean.Expr

Equations

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

def reconstructProof (state : Duper.ProverM.State) : Lean.MetaM Lean.Expr

Given the ProverM state of a duper instance that found a contradiction, reconstruct the proof that duper found and return it as an expression.

Equations

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