Skip to content

Instantly share code, notes, and snippets.

@MarcelineVQ

MarcelineVQ/def.idr

Created August 31, 2019 18:45
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save MarcelineVQ/19d59a14f994fcd01521a05f0b945da9 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
def.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 -> IsSucc n -> Void
try_contradict Uuuh ItIsSucc impossible
try_contradict (Aaah f g {y=Z} {w=Z} {x = Z}) ItIsSucc = ?valid1
try_contradict (Aaah f g {y=Z} {w=Z} {x = (S k)}) ItIsSucc = ?valid2
try_contradict (Aaah f g {y=Z} {w=S k}) ItIsSucc impossible
try_contradict (Aaah f g {y=S j} {w=Z}) ItIsSucc impossible
try_contradict (Aaah f g {y=S j} {w=S k}) ItIsSucc impossible
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment