diff options
| author | Josh Chen | 2020-05-27 21:31:35 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-27 21:31:35 +0200 |
| commit | 62c1c8f306bff84b74b3b1c935d0d6722e1251a2 (patch) | |
| tree | 2a5312d76e7883a000517887d71e84ff2e892a56 /hott/More_Types.thy | |
| parent | ec7dcd5e780d26e7f8866c3d245b08b23de56ff9 (diff) | |
1. Define Maybe in terms of other types. 2. Move More_Types to Spartan
Diffstat (limited to '')
| -rw-r--r-- | spartan/data/More_Types.thy (renamed from hott/More_Types.thy) | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/hott/More_Types.thy b/spartan/data/More_Types.thy index d29d794..f0cee6d 100644 --- a/hott/More_Types.thy +++ b/spartan/data/More_Types.thy @@ -44,7 +44,7 @@ axiomatization where lemmas [intros] = SumF Sum_inl Sum_inr and - [elims] = SumE and + [elims ?s] = SumE and [comps] = Sum_comp_inl Sum_comp_inr @@ -75,7 +75,8 @@ and lemmas [intros] = TopF TopI BotF and - [elims] = TopE BotE and + [elims ?a] = TopE and + [elims ?x] = BotE and [comps] = Top_comp |