[isabelle] lift_definition + constructor



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)"
using coeff_almost_everywhere_zero by (rule
almost_everywhere_zero_nat_case)

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 datatype_new ?

Walther

PS: For those who find the question strange: If there is a "yes" then we could have a mCons for distributive representation of polynomials.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.