Email Gateway (Aug 22 2022 at 17:41): 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: Apr 25 2024 at 12:23 UTC