Skip to content

Instantly share code, notes, and snippets.

@sellout

sellout/gist:4ebcade5736875af4fc2

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/4ebcade5736875af4fc2 to your computer and use it in GitHub Desktop.
Save sellout/4ebcade5736875af4fc2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.idr
tightmod : Nat -> (m : Nat) -> Not (m = Z) -> Fin m
tightmod _ Z prf = FalseElim (prf refl)
tightmod left (S modulus) p = case decLTE left (S modulus) of
Yes _ => fromMaybe fZ (natToFin left (S modulus))
No _ => tightmod (left - (S modulus)) (S modulus) p
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment