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,
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
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 to.
