mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
Remove decideLTE
(#3031)
This commit is contained in:
parent
870bc82437
commit
4fcb0fb4a7
@ -22,12 +22,6 @@ ltesuccinjective : {0 n, m : Nat} -> Not (LTE n m) -> Not (LTE (S n) (S m))
|
||||
ltesuccinjective disprf (LTESucc nLTEm) = void (disprf nLTEm)
|
||||
ltesuccinjective disprf LTEZero impossible
|
||||
|
||||
-- Remove any time after release of 0.6.0
|
||||
||| Deprecated. Use `Nat.isLTE`.
|
||||
public export
|
||||
decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
|
||||
decideLTE = isLTE
|
||||
|
||||
||| If a predicate is decidable then we can decide whether it holds on
|
||||
||| a bounded domain.
|
||||
public export
|
||||
@ -58,11 +52,11 @@ decideLTEBounded pdec n with (decideLTBounded pdec (S n))
|
||||
|
||||
public export
|
||||
Decidable 2 [Nat,Nat] LTE where
|
||||
decide = decideLTE
|
||||
decide = isLTE
|
||||
|
||||
public export
|
||||
Decidable 2 [Nat,Nat] LT where
|
||||
decide m = decideLTE (S m)
|
||||
decide m = isLTE (S m)
|
||||
|
||||
public export
|
||||
lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
|
||||
|
Loading…
Reference in New Issue
Block a user