Hi Christian,
the two different size functions become relevant as soon as you have a polymorphic
datatype such as
datatype 'a foo = Foo 'a | Bar 'a foo
Then, foo_size takes size function for every type variable as additional parameters and
takes them into account, whereas size ignores
Hi Florian,
An example could be something like
primitive_recursion card :: 'a set = nat
where
card {} = 0
card (insert x A) = Suc (card A)
proof -
show !!x y. insert x o insert y = insert y o insert x
show !!x. insert x o insert x = insert x
qed
thm card.simps -- {*
card {} =
Hi Andreas,
Thanks a lot! This fills a knowledge gap. ;o)
I am happy to keep the status quo. But I guess in an ideal world
one would then have two names for the associated theorems. Then
size would fit in with every other simp-theorems coming from
function or primrec definitions.
Thanks
Am 05.08.2013 um 18:02 schrieb Makarius makar...@sketis.net:
On Sun, 4 Aug 2013, Fabian Immler wrote:
I think it is a good idea to inform everyone here that a current student's
project is about to provide a bit more advanced user interface for the find
theorems functionality. It should be
On Fri, 2 Aug 2013, Christian Sternagel wrote:
On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of
such useful tools.
Do you
Hi Jasmin,
On 07/30/2013 05:40 PM, Jasmin Christian Blanchette wrote:
A rough, optimistic time plan follows.
[...]
Wow, I'm looking forward to it!
Let me quickly review the dependencies of the function package on the
datatype package:
- The package registers a datatype interpretation to
Hi Alex,
- The package registers a datatype interpretation to generate congruence
rules the case combinator for each type.
I guess it would make sense to have the package do that, or is there a specific
reason why it is better to do it in a function-related extension?
- The pattern
Dear Makarius,
actually even more is missing, since I was not able to properly use hg
export (I am used to hg bundle which exports *all* changesets that
are only local, whereas for hg export I have to give all revisions
that should be exported explicitly). Sorry for that. Please find
