Idris2Doc : Spidr.Data.Nat

Spidr.Data.Nat

(source)
Nat definitions.

Reexports

import public Data.Nat

Definitions

0 Neq : Nat -> Nat -> Type
  A `Neq x y` proves `x` is not equal to `y`.

Totality: total
Visibility: public export
gtIsSucc : GT x y -> IsSucc x
Totality: total
Visibility: export
multSuccIsSucc : IsSucc x -> IsSucc y -> IsSucc (x * y)
Totality: total
Visibility: export