Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
On 2/13/2014 9:14 AM, Ondřej Kunčar wrote:
The problem is addressed in 6ea67a791108.
To work with the repository, I was thinking I'd have to do something
complex, but then I just downloaded the 2 changeset files and built the
image. Also, thanks for the heads up on `minus` causing problems. That
may not be applicable here, but I'm sure it'll come up in the future.
Dude expressions are applicable, and possibly Fabian Cancellera
analogies, or maybe not, as I tend to confuse Czechoslovakia with the
Swiss domain .ch, but we can say that the power of the lifting package
can be compared to the size of André Greipel's thighs. As to the speed
with which I instantiated my type as `linordered_semidom`, we can say
that is comparable to the speed of Marcel Kittel.
There actually would have been a big snag, except for a recent tip by
Andreas Lochbihler, to not use ==> in a structured proof, but to use
`assume`. A proof goal was going all crazy when I would prove the step
The numeral type class is also important, by Florain Haftmann and Brian
Huffman. I haven't figured it out yet, but I know not to let my simp
rules interfere with letting it do its job.
Having a set of constants for a number system is a big reason why one
traditionally has to resort to using integers, rational numbers, and
real numbers. It's rather radical to have a set of constants, the
numerals, that are both abstract, due to polymorphism, but yet can be
used concretely. If I never have to use the real numbers or rational
numbers, because I can figure out how to get by with the numerals,
that'll be fine with me.
This archive was generated by a fusion of
Pipermail (Mailman edition) and