quox/lib/Quox/NatExtra.idr

33 lines
724 B
Idris
Raw Normal View History

2022-04-11 17:33:32 -04:00
module Quox.NatExtra
import public Data.Nat
2022-05-02 16:38:37 -04:00
%default total
2022-04-11 17:33:32 -04:00
public export
data LTE' : Nat -> Nat -> Type where
LTERefl : LTE' n n
LTESuccR : LTE' m n -> LTE' m (S n)
%builtin Natural LTE'
2022-04-12 10:48:23 -04:00
public export %hint
2022-04-11 17:33:32 -04:00
lteZero' : {n : Nat} -> LTE' 0 n
lteZero' {n = 0} = LTERefl
lteZero' {n = S n} = LTESuccR lteZero'
2022-04-12 10:48:23 -04:00
public export %hint
2022-04-11 17:33:32 -04:00
lteSucc' : LTE' m n -> LTE' (S m) (S n)
lteSucc' LTERefl = LTERefl
lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p
public export
2022-04-23 18:21:30 -04:00
fromLte : {n : Nat} -> LTE m n -> LTE' m n
fromLte LTEZero = lteZero'
fromLte (LTESucc p) = lteSucc' $ fromLte p
2022-04-11 17:33:32 -04:00
public export
toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
toLte LTERefl = reflexive
toLte (LTESuccR p) = lteSuccRight (toLte p)