I've had a quick scan over the NICTA repositories. It doesn't look like
there are any live original uses of recdef. There are recdefs in a copy
of Simpl-AFP, and in some backups of historical papers.
Short summary, NICTA doesn't have any stakes in recdef.
Cheers,
Thomas.
On 08/06/15 06:13,
On 06/06/15 17:11, Florian Haftmann wrote:
So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow? Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed
A frequent use case is this: you have 5-10 interesting patterns where stuff
happens and an otherwise pattern with a simple rhs. In that case you do want to
write those 5-10 patterns explicitly and let the definition facility take care
of the hundreds of patterns that the default case expands
The syntax is nice, but I would interpret _⇩ℕ not as of_nat but as
into nat, or more specifically I would read: _⇩ℝ == real _.
- Johannes
Am Freitag, den 05.06.2015, 23:58 +0200 schrieb Florian Haftmann:
Hi again,
after I first iteration of discussion I see a list of three requirements:
