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