Skip to content

Instantly share code, notes, and snippets.

@MarcelineVQ

MarcelineVQ/fsdf.idr

Created August 31, 2019 19:11
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save MarcelineVQ/f0ee096729532b5e3166a216c7fc408f to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save MarcelineVQ/f0ee096729532b5e3166a216c7fc408f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
fsdf.idr
data Foo : Nat -> Nat -> Type where
Uuuh : Foo Z 0
Aaah : Foo x y -> Foo x w -> Foo (S x) (y+w)
try_contradict : Foo n 0 -> (n = S Z) -> Void
try_contradict Uuuh Refl impossible
try_contradict (Aaah f g {y=Z} {w=Z} {x = Z}) prf = ?valid1
try_contradict (Aaah f g {y=Z} {w=Z} {x = (S k)}) prf = (\Refl impossible) prf
try_contradict (Aaah f g {y=Z} {w=S k}) prf impossible
try_contradict (Aaah f g {y=S j} {w=Z}) prf impossible
try_contradict (Aaah f g {y=S j} {w=S k}) prf impossible
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment