Idris2Doc : Data.Refined.Nat

Data.Refined.Nat

(source)
Reexports
import public Data.Nat
import public Data.Refined.Core
Definitions
fromLTE : (k : Nat) -> (v : Nat) -> {auto 0 _ : k <= v = True} -> LTE k v
  Totality: total
  Visibility: public export