inductive Duper.SimpResult (α : Type) : Type

• Applied {α : Type} (c : α) : SimpResult α
• Unapplicable {α : Type} : SimpResult α
• Removed {α : Type} : SimpResult α

instance Duper.instInhabitedSimpResult {a✝ : Type} : Inhabited (SimpResult a✝)

Equations

• Duper.instInhabitedSimpResult = { default := Duper.SimpResult.Unapplicable }

def Duper.SimpResult.mapM {m : Type → Type u_1} {α β : Type} [Monad m] (f : α → m β) : SimpResult α → m (SimpResult β)

Equations

• Duper.SimpResult.mapM f (Duper.SimpResult.Applied c) = do let __do_lift ← f c pure (Duper.SimpResult.Applied __do_lift)
• Duper.SimpResult.mapM f Duper.SimpResult.Unapplicable = pure Duper.SimpResult.Unapplicable
• Duper.SimpResult.mapM f Duper.SimpResult.Removed = pure Duper.SimpResult.Removed

def Duper.SimpResult.forM {m : Type u → Type v} [Monad m] {α : Type} (r : SimpResult α) (f : α → m PUnit) : m PUnit

Equations

• (Duper.SimpResult.Applied c).forM f = f c
• Duper.SimpResult.Unapplicable.forM f = pure PUnit.unit
• Duper.SimpResult.Removed.forM f = pure PUnit.unit

@[reducible, inline]

abbrev Duper.MSimpRule : Type

Equations

• Duper.MSimpRule = (Duper.Clause → Duper.RuleM.RuleM (Option (Array (Duper.Clause × Duper.RuleM.Proof))))

@[reducible, inline]

abbrev Duper.SimpRule : Type

Equations

• Duper.SimpRule = (Duper.Clause → Duper.ProverM.ProverM (Duper.SimpResult Duper.Clause))

@[reducible, inline]

abbrev Duper.BackwardMSimpRule : Type

Equations

• Duper.BackwardMSimpRule = (Duper.Clause → Duper.RuleM.RuleM (Array (Duper.Clause × Option (Duper.Clause × Duper.RuleM.Proof))))

@[reducible, inline]

abbrev Duper.BackwardSimpRule : Type

Equations

• Duper.BackwardSimpRule = (Duper.Clause → Duper.ProverM.ProverM Unit)

def Duper.MSimpRule.toSimpRule (rule : MSimpRule) : SimpRule

Equations

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

def Duper.MSimpRule.toPreprocessingSimpRule (rule : MSimpRule) : SimpRule

Like MSimpRule.toSimpRule, but extra clauses are added to the set of unsupported facts rather than the passive set.

Equations

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

def Duper.BackwardMSimpRule.toBackwardSimpRule (rule : BackwardMSimpRule) : BackwardSimpRule

Equations

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