# [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.*