Documentation

Std.Tactic.BVDecide.LRAT.Internal.PosFin

source
def Std.Tactic.BVDecide.LRAT.Internal.PosFin (n : Nat) :
Type
Equations
    Instances For
      source
      instance Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqPosFin {n : Nat} :
      DecidableEq (PosFin n)
      Equations
        source
        instance Std.Tactic.BVDecide.LRAT.Internal.instCoeOutPosFinNat {n : Nat} :
        CoeOut (PosFin n) Nat
        Equations
          source
          instance Std.Tactic.BVDecide.LRAT.Internal.instHashablePosFin {n : Nat} :
          Hashable (PosFin n)
          Equations
            source
            instance Std.Tactic.BVDecide.LRAT.Internal.instToStringPosFin {n : Nat} :
            ToString (PosFin n)
            Equations