source
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

source
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 })

source
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 }

source
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 }

source
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 }