diff options
| author | Josh Chen | 2018-08-16 19:45:11 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-16 19:45:11 +0200 |
| commit | 096ce05cb57c101e13d308b5df7a7af2a0060bf2 (patch) | |
| tree | 490baf135535545629775977b1176eebef8a6948 | |
| parent | d8699451025a3bd5e8955e07fa879ed248418949 (diff) | |
test new machine
| -rw-r--r-- | HoTT_Test.thy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/HoTT_Test.thy b/HoTT_Test.thy index 4c87e78..bce2f00 100644 --- a/HoTT_Test.thy +++ b/HoTT_Test.thy @@ -50,6 +50,8 @@ by (simple lems: assms) subsection \<open>Function application\<close> +text "silly test" + proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (simple lems: assms) text "Currying:" |