Re: [isabelle] lift_definition + constructor
thanks for your hints !
In the course of general considerations  we come back to this
On 11/19/2013 08:24 PM, Brian Huffman wrote:
On Tue, Nov 19, 2013 at 9:57 AM, Walther Neuper <wneuper at ist.tugraz.at> wrote:
In Isabelle2013-1 in HOL/Library/Polynomial there is
lift_definition pCons :: "'a::zero => 'a poly => 'a poly"
is "λa p. nat_case a (coeff p)"
Other kinds of representations, for instance sparse distributive
polynomial representation like , could be lifted as well
(establishing respective morphisms) by something like
lift_definition dCons :: "..."
and then there is the question, how to distinguish between "pCons" and
"dCons": pattern matching, for instance by ...
case p of
pCons _ => ...
| dCons _ => ...
... on constructors "pCons" and "dCons" was an idea ...
Is there a way to have a constructor "pCons" instead of function "pCons"?
I.e. a constructor like
datatype 'a pcons = Zero | pCons 'a "'a pcons"
could be somehow associated with lift_definition ? Or is this possible with
What exactly do you mean by "constructor"? HOL doesn't have any
built-in logical distinction between constructors and other functions.
The signatures of pCons, dCons, etc are under question, also the
location with respect to the lift_definition --- do you find anything
realisable about this idea ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and