diff options
| author | Josh Chen | 2019-03-26 17:04:01 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-03-26 17:04:01 +0100 |
| commit | 45c3879db6850282bc067318e31cccf42e60ac8f (patch) | |
| tree | fd7753a339ee8a0e90bb97f80fc4105666ed7288 /Projections.thy | |
| parent | 6dd1b27f7f84b17ad88e5b382042bd0c577a92f4 (diff) | |
working towards biinv_imp_qinv
Diffstat (limited to 'Projections.thy')
| -rw-r--r-- | Projections.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Projections.thy b/Projections.thy index a28c66b..c89b569 100644 --- a/Projections.thy +++ b/Projections.thy @@ -11,10 +11,10 @@ imports Prod Sum begin -definition fst ("(2fst[_, _])") +definition fst ("(2fst[_,/ _])") where "fst[A, B] \<equiv> \<lambda>(p: \<Sum>x: A. B x). indSum (\<lambda>_. A) (\<lambda>x y. x) p" -definition snd ("(2snd[_, _])") +definition snd ("(2snd[_,/ _])") where "snd[A, B] \<equiv> \<lambda>(p: \<Sum>x: A. B x). indSum (\<lambda>p. B (fst[A, B]`p)) (\<lambda>x y. y) p" lemma fst_type: |