aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-06-07 19:37:07 +0200
committerJosh Chen2018-06-07 19:37:07 +0200
commit012916d1ad08edcb68b8be6251ba457c0c0783f0 (patch)
tree2d918066dacfda64f1872dfff7218021f86db7e2
parentfc19fe90e7cb13acc03deaf061b2b6cf3df2d165 (diff)
But also looser than Pair
-rw-r--r--HoTT.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/HoTT.thy b/HoTT.thy
index c1c6e72..44f55e9 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -57,7 +57,7 @@ translations
"%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
(* The above syntax translations bind the x in the expressions B, b. *)
-abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 80)
+abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40)
where "A\<rightarrow>B \<equiv> \<Prod>_:A. B"
axiomatization