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
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 splitt
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 gene
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 f
Am 05.08.2013 um 18:02 schrieb Makarius :
> 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 finished in
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 agai
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 finished in two weeks
time.
So far I only know about the existe
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.si
