def Std.Tactic.BVDecide.LRAT.Internal.PosFin (n : Nat) : Type

Equations

• Std.Tactic.BVDecide.LRAT.Internal.PosFin n = { x : Nat // 0 < x ∧ x < n }

Instances For

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.instEntailsPosFinArray
• Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.instClausePosFin
• Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instEntailsPosFin
• Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instFormulaPosFinDefaultClause
• Std.Tactic.BVDecide.LRAT.Internal.instCoeOutPosFinNat
• Std.Tactic.BVDecide.LRAT.Internal.instHashablePosFin
• Std.Tactic.BVDecide.LRAT.Internal.instToStringPosFin

instance Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqPosFin {n : Nat} : DecidableEq (PosFin n)

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqPosFin = inferInstanceAs (DecidableEq { x : Nat // 0 < x ∧ x < n })

instance Std.Tactic.BVDecide.LRAT.Internal.instCoeOutPosFinNat {n : Nat} : CoeOut (PosFin n) Nat

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instCoeOutPosFinNat = { coe := fun (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) => p.val }

instance Std.Tactic.BVDecide.LRAT.Internal.instHashablePosFin {n : Nat} : Hashable (PosFin n)

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instHashablePosFin = { hash := fun (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) => hash p.val }

instance Std.Tactic.BVDecide.LRAT.Internal.instToStringPosFin {n : Nat} : ToString (PosFin n)

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instToStringPosFin = { toString := fun (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) => toString p.val }