Skip to content

Instantly share code, notes, and snippets.

@NicolaiNebel

NicolaiNebel/peano_equal.agda

Created April 11, 2017 12:49
Show Gist options
  • Save NicolaiNebel/51cbdd403114306c06aadaebeb3ce86a to your computer and use it in GitHub Desktop.
Save NicolaiNebel/51cbdd403114306c06aadaebeb3ce86a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
peano_equal.agda
module peano_equal where
data Nat : Set where
z : Nat
s : Nat -> Nat
record True where
constructor T
data False where
PEq : Nat -> Nat -> Set
PEq z z = True
PEq (s _) z = False
PEq z (s _) = False
PEq (s n) (s m) = PEq n m
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment