Finish creating the Isabelle/GD tooling to support the definition of new algebraic datatypes automatically, following the syntax and semantics of the datatetype construct in Isabelle/HOL. Perhaps start with a List type, the foundations for which @skehrli developed in his thesis.
Finish creating the Isabelle/GD tooling to support the definition of new algebraic datatypes automatically, following the syntax and semantics of the
datatetypeconstruct in Isabelle/HOL. Perhaps start with a List type, the foundations for which @skehrli developed in his thesis.