equal
deleted
inserted
replaced
53 *} |
53 *} |
54 |
54 |
55 datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex; |
55 datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex; |
56 |
56 |
57 text{*\noindent |
57 text{*\noindent |
58 The evaluation if If-expressions proceeds as for @{typ"boolex"}: |
58 The evaluation of If-expressions proceeds as for @{typ"boolex"}: |
59 *} |
59 *} |
60 |
60 |
61 consts valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool"; |
61 consts valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool"; |
62 primrec |
62 primrec |
63 "valif (CIF b) env = b" |
63 "valif (CIF b) env = b" |