← Copula mathematical handbook

@[implicit_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqPosFin = Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqPosFin._aux_1

@[instance_reducible]

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_reducible]

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_reducible]

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 }