Right, thanks for setting me straight. This is less invasive than I thought.
So the remaining question is, are we happy with replacements like
%x. Suc _ + x ~> Suc _ + _
and proper eta contraction. Both would return potentially more matches, but not
fewer. For eta contraction, we can argue tha
Hi Christian,
> I'm mostly guessing here. Maybe somebody with deeper knowledge of the
> system could comment whether this would be feasible (and also the right
> way to go).
I have not spent much thought on the code, but tried to take a bird's
perspective.
The whole matter is about overloaded ab
Hi Gerwin,
> Do I read find_eta.txt right that the eta expansion is applied to all
patterns? If yes, then that is a problem, because now partially applied
constants won’t be found any more (i.e. the occurrence of `Suc` in `map
Suc ?xs` would be missed if you make it always search for `Suc _`).
It
> Am 27.11.2014 um 00:06 schrieb Gerwin Klein :
>
>> I wonder if it would be feasible to create a regression test for interactive
>> commands like find_theorems so this noticed earlier, but that is a different
>> topic.
>
> We have regression tests for a number of other interactive diagnosis co
Hi Gerwin,
Am 27.11.2014 um 00:06 schrieb Gerwin Klein :
> I wonder if it would be feasible to create a regression test for interactive
> commands like find_theorems so this noticed earlier, but that is a different
> topic.
We have regression tests for a number of other interactive diagnosis c
Hi Florian,
thanks for looking at that.
Do I read find_eta.txt right that the eta expansion is applied to all patterns?
If yes, then that is a problem, because now partially applied constants won’t
be found any more (i.e. the occurrence of `Suc` in `map Suc ?xs` would be
missed if you make it
In Isabelle/5b649fb2f2e1 we now have @{apply n} and @{apply n(k)} to map
all tuple components or one specified tuple component.
In Isabelle/a78612c67ec0 the old "pairself" is renamed to "apply2" to fit
into this scheme. Thus it is also analagous to @{map 2} vs. plain map2 --
these ML combinat
Not sure about lxbroy10, but AODV is now the longest session. It takes about
1:40h on my machine (needs less memory than JinjaThreads, though).
Cheers,
Gerwin
> On 27.11.2014, at 05:10, Florian Haftmann
> wrote:
>
> How long is session AODV expected to run on a machine such as lxbroy10?
> It s
On Wed, 26 Nov 2014, Florian Haftmann wrote:
How long is session AODV expected to run on a machine such as lxbroy10?
It seems to exceed JinjaThreads significantly…
Quite impressive, isn't it? One of my local caches has this timing:
elapsed=10142.147 cpu=38679.631 gc=3478.939
I already start
* Florian Haftmann [2014-11-26
19:40 +0100]:
> @Timothy: in the progress of investigating I stumbled over your
> changeset (c61fe520602b, actually brought in by Gerwin) and dismantled
> it. Do you remember what it had been intended for resp. by which
> criterion we can decide whether the dismant
The following is based against 43e07797269b. If you do not want apply
the patched just copy find_theorems.ML to src/Pure/Tools.
I merely implemented that patterns which are abstractions (after
eta-contraction!) are implicitly expanded with schematic parameters.
Hence
inj ~> %f. inj_on f UNIV
How long is session AODV expected to run on a machine such as lxbroy10?
It seems to exceed JinjaThreads significantly…
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digita
I'm diving into it…
Florian
On 21.11.2014 23:56, Makarius wrote:
> On Sat, 15 Nov 2014, Gerwin Klein wrote:
>
>> I agree that it would be nice to support that, esp since find_theorems
>> is supposed to help beginners find things.
>>
>> Applying underscores will have unwanted side effects
Hi Andreas, hi Jasmin,
> It's quite nice as it is. Thanks!
>
> Andreas: I think I promised to help you with the code generator and
> "code_datatype" (cf. our private email conversation about "Quickcheck &
> Codatatypes"). I don't understand "code_datatype" (or what you do with it)
> well enoug
It had been a lapsus. Regression is under way.
Florian
On 26.11.2014 15:39, Florian Haftmann wrote:
> Hi Dmitriy,
>
> thanks for figuring out. I am currently having a look at it…
>
> Florian
>
> On 20.11.2014 17:34, Dmitriy Traytel wrote:
>> Sorry for reviving an ancient thread
Hi Dmitriy,
thanks for figuring out. I am currently having a look at it…
Florian
On 20.11.2014 17:34, Dmitriy Traytel wrote:
> Sorry for reviving an ancient thread, but have the constants defined by
> inductive ever been visible to find_consts since Florian's commit (I
> presume 4a37475
16 matches
Mail list logo
