Skip to content

Instantly share code, notes, and snippets.

@ka9e

ka9e/Main.agda

Created April 2, 2015 13:41
Show Gist options
  • Save ka9e/cacf508b74e7fb94c5ad to your computer and use it in GitHub Desktop.
Save ka9e/cacf508b74e7fb94c5ad to your computer and use it in GitHub Desktop.
Download ZIP
reflexive
Raw
Main.agda
-- reference : http://d.hatena.ne.jp/ranha/20091010/1255161992
module Main where
data Id {A : Set} (x : A) : A → Set where
refl : Id x x
reflexive : (A : Set) → (x : A) → Id x x
reflexive A x = refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment