[isabelle] Nominal Isabelle and pair types
I am experimenting with using Nominal Isabelle for labelled deductive
systems. For starters, I am trying to create a pair type of labels and
The following definition seems to work:
atom_decl simple_label prop_var
datatype formula = Atom "prop_var"
| Impl "formula" "formula"
| Conj "formula" "formula"
| Disj "formula" "formula"
nominal_datatype labelled_formula =
"\<guillemotleft>simple_label\<guillemotright> * formula"
but them I am unable to use fst (and snd?) on the pair. I get type
unification errors from the following:
get_label :: "labelled_formula \<Rightarrow> simple_label"
"get_label lf \<equiv> (fst lf)"
get_formula :: "labelled_formula \<Rightarrow> formula"
"get_formula lf \<equiv> (snd lf)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and