equal
deleted
inserted
replaced
724 |
724 |
725 |
725 |
726 subsubsection {* Code generator setup *} |
726 subsubsection {* Code generator setup *} |
727 |
727 |
728 definition |
728 definition |
729 is_none :: "'a option \<Rightarrow> bool" |
729 is_none :: "'a option \<Rightarrow> bool" where |
730 is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" |
730 is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" |
731 |
731 |
732 lemma is_none_code [code]: |
732 lemma is_none_code [code]: |
733 shows "is_none None \<longleftrightarrow> True" |
733 shows "is_none None \<longleftrightarrow> True" |
734 and "is_none (Some x) \<longleftrightarrow> False" |
734 and "is_none (Some x) \<longleftrightarrow> False" |