Mercurial > hg > Papers > 2017 > atton-master

annotate paper/src/AgdaImplicitId.agda @ 104:0ab2de92120b teacher-submit

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added tag 1F-submit for changeset 0a4646310261
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 13 Feb 2017 10:33:15 +0900
parents 10a550bf7e4a
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
52
fb42478e4c96 Writing agda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 id : {A : Set} -> A -> A
fb42478e4c96 Writing agda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 id x = x
fb42478e4c96 Writing agda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
64
10a550bf7e4a Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
4 id-zero : Nat
10a550bf7e4a Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
5 id-zero = id zero
10a550bf7e4a Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
6
10a550bf7e4a Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
7 id' : {A : Set} -> A -> A
10a550bf7e4a Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
8 id' {A} x = x
10a550bf7e4a Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
9
52
fb42478e4c96 Writing agda description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 id-true : Bool
64
10a550bf7e4a Mini fixes with ryokka-san
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 52
diff changeset
11 id-true = id {Bool} true