diff options
| -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:" |