diff options
| author | Josh Chen | 2020-05-27 22:16:42 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-27 22:16:42 +0200 |
| commit | f12983b1b53c71fc416155ac4b7e2b11ed8ca9ef (patch) | |
| tree | aa8370faefd779bbdf45676e77001c25a4d3f5cc /spartan/data/Maybe.thy | |
| parent | ed41980ed5cee12d7c5eea2e40627e5a390a83f8 (diff) | |
change variable name in elim rules and fix small mistake
Diffstat (limited to '')
| -rw-r--r-- | spartan/data/Maybe.thy | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/spartan/data/Maybe.thy b/spartan/data/Maybe.thy index dc3ad04..98f5283 100644 --- a/spartan/data/Maybe.thy +++ b/spartan/data/Maybe.thy @@ -1,8 +1,12 @@ +chapter \<open>Maybe type\<close> + theory Maybe imports More_Types begin +text \<open>Defined as a sum.\<close> + definition "Maybe A \<equiv> A \<or> \<top>" definition "none A \<equiv> inr A \<top> tt" definition "some A a \<equiv> inl A \<top> a" |