Idris2Doc : Data.Nat1

Data.Nat1

(source)
Reexports
import public Data.Nat
import public Data.DPair
import public Data.So
Definitions
data Nat1 : Type
  Totality: total
  Visibility: public export
  Constructor: 
FromNat : (n : Nat) -> {auto 0 _ : IsSucc n} -> Nat1

  Hints:
  
Eq Nat1
  
Ord Nat1
  
Range Nat1
toNat1 : Nat -> Maybe Nat1
  Totality: total
  Visibility: public export
fromNat : (x : Nat) -> {auto 0 _ : IsSucc x} -> Nat1
  Totality: total
  Visibility: public export
.asNat : Nat1 -> Nat
  Totality: total
  Visibility: public export
toNat : Nat1 -> Nat
  Totality: total
  Visibility: public export
fromInteger : (x : Integer) -> {auto 0 _ : So (x >= 1)} -> Nat1
  Totality: total
  Visibility: public export
succ : Nat1 -> Nat1
  Totality: total
  Visibility: public export
one : Nat1
  Totality: total
  Visibility: public export
(+) : Nat1 -> Nat1 -> Nat1
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 8
(*) : Nat1 -> Nat1 -> Nat1
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 9
gcd : (a : Nat) -> (b : Nat) -> {auto 0 _ : Either (IsSucc a) (IsSucc b)} -> Nat1
  Totality: total
  Visibility: export
gcd' : Nat1 -> Nat1 -> Nat1
  Totality: total
  Visibility: export
pickWeighted : LazyLst1 (Nat1, a) -> Nat -> a
  Totality: total
  Visibility: export
normaliseWeights : Foldable f => Functor f => f (Nat1, a) -> f (Nat1, a)
  Totality: total
  Visibility: export