Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Nominal2 and Code Generation

Email Gateway (Aug 22 2022 at 17:41):

From: Mark Wassell <mpwassell@gmail.com>
Hello,

Is it possible to generate code from nominal datatypes and inductive
predicates defined over them?

The very basic datatype and inductive predicate below doesn't generate code
for mode i whereas it does for a non-Nominal version.

I understand that nominal2 datatypes are built using quotient types so
should I be looking at how code generation with inductive predicates over
quotient types works?

Cheers

Mark

nominal_datatype "foo" =
Bar
| Baz int foo

inductive R :: "foo ⇒ bool" where
"R Bar"
| "⟦ i ≥ 0 ; R fs ⟧ ⟹ R (Baz i fs)"
equivariance R
nominal_inductive R .

code_pred [show_steps, show_mode_inference, show_invalid_clauses] R .

Last updated: Nov 21 2024 at 12:39 UTC