From: Florian Haftmann <email@example.com>
in certain applications (most prominently polynomials) almost everywhere
constant functions nat => 'a play a critical role, and any almost
everywhere constant function can be assigned a degree, i. e. the highest
n such that for any higher n the function is constant.
Is there any stand-alone formalizsation of this concept?
From: Manuel Eberl <firstname.lastname@example.org>
The only thing I am aware of is HOL-Library.Poly_Mapping, which you are
probably aware of, seeing as it has your name at the top.
Last updated: Jul 15 2022 at 23:21 UTC