rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

make lteZero' and lteSucc' into hints

Browse source
This commit is contained in:
rhiannon morris 2022-04-12 16:48:23 +02:00
parent de6ec78e23
commit 56ddd59fb4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Quox/NatExtra.idr
View file

@ -9,12 +9,12 @@ data LTE' : Nat -> Nat -> Type where
LTESuccR : LTE' m n -> LTE' m (S n) LTESuccR : LTE' m n -> LTE' m (S n)
%builtin Natural LTE' %builtin Natural LTE'
public export public export %hint
lteZero' : {n : Nat} -> LTE' 0 n lteZero' : {n : Nat} -> LTE' 0 n
lteZero' {n = 0} = LTERefl lteZero' {n = 0} = LTERefl
lteZero' {n = S n} = LTESuccR lteZero' lteZero' {n = S n} = LTESuccR lteZero'
public export public export %hint
lteSucc' : LTE' m n -> LTE' (S m) (S n) lteSucc' : LTE' m n -> LTE' (S m) (S n)
lteSucc' LTERefl = LTERefl lteSucc' LTERefl = LTERefl
lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p