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

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

instance Std.Tactic.BVDecide.LRAT.Internal.instCoeOutPosFinNat {n : Nat} : CoeOut (Std.Tactic.BVDecide.LRAT.Internal.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.instToStringPosFin {n : Nat} : ToString (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)

Equations

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