comparison Paper/src/AgdaImplicitId.agda @ 1:bf2887cd22c1

fix Paper
author ryokka
date Fri, 13 Apr 2018 19:47:50 +0900
parents
children
comparison
equal deleted inserted replaced
0:a5facba1adbc 1:bf2887cd22c1
1 id : {A : Set} -> A -> A
2 id x = x
3
4 id-zero : Nat
5 id-zero = id zero
6
7 id' : {A : Set} -> A -> A
8 id' {A} x = x
9
10 id-true : Bool
11 id-true = id {Bool} true