diff options
author | Josh Chen | 2018-06-17 00:48:01 +0200 |
---|---|---|
committer | Josh Chen | 2018-06-17 00:48:01 +0200 |
commit | 5161a0356d8752f3b1b4f4385e799bca92718814 (patch) | |
tree | c7cf1dfd80311af85dd81229ec8f1302395c1c9f /Prod.thy | |
parent | 602ad9fe0e2ed1ad4ab6f16e720de878aadc0fba (diff) |
Decided on a new proper scheme for type rules using the idea of implicit well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.
Diffstat (limited to 'Prod.thy')
-rw-r--r-- | Prod.thy | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -33,7 +33,7 @@ translations axiomatization where Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U" and - Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b x : B x) \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x" + Prod_intro [intro]: "\<And>A B b. \<lbrakk>A : U; \<And>x. x : A \<Longrightarrow> b x : B x\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x" and Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a" and |