Skip to content

Instantly share code, notes, and snippets.

@sellout

sellout/gist:11408315

Last active August 29, 2015 14:00
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save sellout/11408315 to your computer and use it in GitHub Desktop.
Save sellout/11408315 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.idr
partial
tightmod : Nat -> (m : Nat) -> so (m /= Z) -> Fin m
tightmod left (S right) p = if left < (S right)
then fromMaybe fZ (natToFin left (S right))
else tightmod (left - (S right)) (S right) p
@david-christiansen
Copy link

-- This might be handy...

%default total

succBiggerZero : LTE (S k) Z -> |
succBiggerZero lteZero impossible
succBiggerZero (lteSucc x) impossible

lteSuccBack : LTE (S k) (S j) -> LTE k j
lteSuccBack (lteSucc x) = x

decLTE : (n, m : Nat) -> Dec (LTE n m)
decLTE Z m = Yes lteZero
decLTE (S k) Z = No succBiggerZero
decLTE (S k) (S j) with (decLTE k j)
decLTE (S k) (S j) | (Yes prf) = Yes $ lteSucc prf
decLTE (S k) (S j) | (No contra) = No $ contra . lteSuccBack

@david-christiansen
Copy link

-- might also be handy

splitLTE : (n, m : Nat) -> Either (LTE n m) (LTE m (S n))
splitLTE Z m = Left lteZero
splitLTE (S k) Z = Right lteZero
splitLTE (S k) (S j) with (splitLTE k j)
splitLTE (S k) (S j) | (Left x) = Left (lteSucc x)
splitLTE (S k) (S j) | (Right x) = Right (lteSucc x)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment