Skip to content

Instantly share code, notes, and snippets.

@ohad

ohad/fails.idr Secret

Created August 20, 2019 15:29
Show Gist options
  • Save ohad/c0053b127c74a2044ecd5a55f50dc74b to your computer and use it in GitHub Desktop.
Save ohad/c0053b127c74a2044ecd5a55f50dc74b to your computer and use it in GitHub Desktop.
Download ZIP
Idris example that fails
Raw
fails.idr
data A : Type where
The : Type -> A
U : A -> Type
U (The x) = x
works : (a : A) -> (H : U a) -> (let q = H in Nat)
works a h = 0
fails : (a : A) -> (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