Skip to content

Instantly share code, notes, and snippets.

@ohad

ohad/works.idr Secret

Created August 20, 2019 15:28
Show Gist options
  • Save ohad/1a238aad4308c7c26fa67f28eb90a3d6 to your computer and use it in GitHub Desktop.
Save ohad/1a238aad4308c7c26fa67f28eb90a3d6 to your computer and use it in GitHub Desktop.
Download ZIP
Idris example that works
Raw
works.idr
U : Type -> Type
U x = x
works : (a : Type) -> (H : U a) -> (let q = H in Nat)
works a h = 0
fails : (a : Type) -> (H : U a) -> (let q : U a = H in Nat)
fails a h = 0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment