opaque Duper.simultaneousSuperposition : Lean.Option Bool

opaque Duper.enableSuperpositionWatchClauses : Lean.Option Bool

opaque Duper.superpositionWatchClause1 : Lean.Option Nat

opaque Duper.superpositionWatchClause2 : Lean.Option Nat

def Duper.getSimultaneousSuperposition (opts : Lean.Options) : Bool

Equations

• Duper.getSimultaneousSuperposition opts = Lean.Option.get opts Duper.simultaneousSuperposition

def Duper.getSimultaneousSuperpositionM : Lean.CoreM Bool

Equations

• Duper.getSimultaneousSuperpositionM = do let opts ← Lean.getOptions pure (Duper.getSimultaneousSuperposition opts)

def Duper.getEnableSuperpositionWatchClauses (opts : Lean.Options) : Bool

Equations

• Duper.getEnableSuperpositionWatchClauses opts = Lean.Option.get opts Duper.enableSuperpositionWatchClauses

def Duper.getSuperpositionWatchClause1 (opts : Lean.Options) : Nat

Equations

• Duper.getSuperpositionWatchClause1 opts = Lean.Option.get opts Duper.superpositionWatchClause1

def Duper.getSuperpositionWatchClause2 (opts : Lean.Options) : Nat

Equations

• Duper.getSuperpositionWatchClause2 opts = Lean.Option.get opts Duper.superpositionWatchClause2

def Duper.getEnableSuperpositionWatchClausesM : Lean.CoreM Bool

Equations

• Duper.getEnableSuperpositionWatchClausesM = do let opts ← Lean.getOptions pure (Duper.getEnableSuperpositionWatchClauses opts)

def Duper.getSuperpositionWatchClause1M : Lean.CoreM Nat

Equations

• Duper.getSuperpositionWatchClause1M = do let opts ← Lean.getOptions pure (Duper.getSuperpositionWatchClause1 opts)

def Duper.getSuperpositionWatchClause2M : Lean.CoreM Nat

Equations

• Duper.getSuperpositionWatchClause2M = do let opts ← Lean.getOptions pure (Duper.getSuperpositionWatchClause2 opts)

def Duper.mkSuperpositionProof (sidePremiseLitIdx : Nat) (sidePremiseLitSide : LitSide) (mainPremisePos : ClausePos) (givenIsMain : Bool) (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

Equations

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

def Duper.mkSimultaneousSuperpositionProof (sidePremiseLitIdx : Nat) (sidePremiseLitSide : LitSide) (givenIsMain : Bool) (poses : Array ClausePos) (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

Equations

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

def Duper.superpositionAtLitWithPartner (mainPremise : MClause) (mainPremiseNum : Nat) (mainPremiseSubterm : Lean.Expr) (mainPremisePos : ClausePos) (mainPremiseEligibility : Eligibility) (sidePremise : MClause) (sidePremiseNum sidePremiseLitIdx : Nat) (sidePremiseSide : LitSide) (sidePremiseEligibility : Eligibility) (given : Clause) (givenIsMain simultaneousSuperposition : Bool) : RuleM.RuleM (Array ClauseStream)

Equations

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

def Duper.superpositionWithGivenAsSide (given : Clause) (mainPremiseIdx : RootCFPTrie) (sidePremise : MClause) (sidePremiseNum sidePremiseLitIdx : Nat) (sidePremiseSide : LitSide) (sidePremiseEligibility : Eligibility) (simultaneousSuperposition : Bool) : RuleM.RuleM (Array ClauseStream)

Equations

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

def Duper.superpositionWithGivenAsMain (given : Clause) (e : Lean.Expr) (pos : ClausePos) (sidePremiseIdx : RootCFPTrie) (mainPremise : MClause) (mainPremiseNum : Nat) (mainPremiseEligibility : Eligibility) (simultaneousSuperposition : Bool) : RuleM.RuleM (Array ClauseStream)

Equations

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

def Duper.superposition (mainPremiseIdx sidePremiseIdx : RootCFPTrie) (given : Clause) (givenClause : MClause) (givenClauseNum : Nat) : RuleM.RuleM (Array ClauseStream)

Equations

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