Documentation

Std.Tactic.BVDecide.LRAT.Internal.PosFin

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

Equations

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

Instances For

instance Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqPosFin {n : Nat} :

DecidableEq (Std.Tactic.BVDecide.LRAT.Internal.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 (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 }