From 831f33468f227c0dc96bd31380236f2c77e70c52 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 9 Jul 2020 13:35:39 +0200 Subject: Non-annotated object lambda --- spartan/lib/Maybe.thy | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'spartan/lib/Maybe.thy') diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy index 6729812..d821920 100644 --- a/spartan/lib/Maybe.thy +++ b/spartan/lib/Maybe.thy @@ -24,7 +24,7 @@ Definition MaybeInd: "c\<^sub>0: C (none A)" "\a. a: A \ f a: C (some A a)" "m: Maybe A" - shows "?MaybeInd A (\m. C m) c\<^sub>0 (\a. f a) m: C m" + shows "C m" supply assms[unfolded Maybe_def none_def some_def] apply (elim m) \ unfolding Maybe_def . @@ -38,7 +38,7 @@ Lemma Maybe_comp_none: "c\<^sub>0: C (none A)" "\a. a: A \ f a: C (some A a)" "\m. m: Maybe A \ C m: U i" - shows "MaybeInd A (\m. C m) c\<^sub>0 (\a. f a) (none A) \ c\<^sub>0" + shows "MaybeInd A C c\<^sub>0 f (none A) \ c\<^sub>0" supply assms[unfolded Maybe_def some_def none_def] unfolding MaybeInd_def none_def by reduce @@ -49,7 +49,7 @@ Lemma Maybe_comp_some: "c\<^sub>0: C (none A)" "\a. a: A \ f a: C (some A a)" "\m. m: Maybe A \ C m: U i" - shows "MaybeInd A (\m. C m) c\<^sub>0 (\a. f a) (some A a) \ f a" + shows "MaybeInd A C c\<^sub>0 f (some A a) \ f a" supply assms[unfolded Maybe_def some_def none_def] unfolding MaybeInd_def some_def by (reduce add: Maybe_def) @@ -62,11 +62,8 @@ lemmas abbreviation "MaybeRec A C \ MaybeInd A (K C)" -definition none_i ("none") - where [implicit]: "none \ Maybe.none ?" - -definition some_i ("some") - where [implicit]: "some a \ Maybe.some ? a" +definition none_i ("none") where [implicit]: "none \ Maybe.none ?" +definition some_i ("some") where [implicit]: "some a \ Maybe.some ? a" translations "none" \ "CONST Maybe.none A" -- cgit v1.2.3