Thanks, I was wondering about that also.
Is there conceptual reason that "Local_Theory.target" is needed, or is
it just kind of technical hiccup?
cheers,
lucas
Jasmin Christian Blanchette wrote:
> Hi all,
>
>> I was trying to make Nitpick more context-friendly and thought that
>> "local_setup" and "Generic_Data" would be my friends. However, "local_setup"
>> seems to do nothing -- the changes I perform to the data are coldly ignored.
>> The little theory below shows illustrates what I mean:
>> [...]
>> local_setup {* Context.proof_map (Data.map (Integer.add 3)) *}
>
> FYI. Florian has explained this to me live. For the record,
>
> local_setup {* Local_Theory.target (Context.proof_map (Data.map
> (Integer.add 3))) *}
>
> or
>
> declaration {* fn phi => Data.map (Integer.add 3) *}
>
> do the trick.
>
> Jasmin
>
> _______________________________________________
> Isabelle-dev mailing list
> [email protected]
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
