Idris2Doc : Data.Fin.Minus

Data.Fin.Minus

(source)
Special subtraction of a `Fin` from a `Nat`

Reexports

import public Data.Fin

Definitions

negate : Neg ty => ty -> ty
  The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.

Totality: total
Visibility: public export
Fixity Declaration: prefix operator, level 10
(-) : (n : Nat) -> Fin (S n) -> Nat
Totality: total
Visibility: public export
Fixity Declarations:
infixl operator, level 8
prefix operator, level 10
plus_discards_minus : (n : Nat) -> (f : Fin (S n)) -> (n - f) + finToNat f = n
Totality: total
Visibility: export
minus_last_gives_0 : (n : Nat) -> n - last = 0
Totality: total
Visibility: export