def Duper.mkFluidSupProof (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.mkFreshFunction (inputTy outputTy : Lean.Expr) : Lean.MetaM Lean.Expr

Returns the dependent lambda expression with the appropriate input and output types

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Duper.fluidSup (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.