[isabelle-dev] "local_setup" and "Generic_Data"

[Lucas Dixon]

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
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> 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.