Re: [isabelle] Strange interaction between Rewrite and Adhoc_Overloading



Dear all,

The easy fix would be to add (but I didn't do anything in the repo,
because I wanted to avoid potential clashes with others).

  hide_const (open) List.nth

at the top of Definedness.thy. The problem was just that we define our
own "nth" (in Data_List) function but since "nth" is also defined in
Main and Definedness imports Adhoc_Overloading after Data_List. No
suddenly "nth" referred to List.nth instead of Data_List.nth.

cheers

chris

On 05/02/2018 10:06 AM, Lars Hupel wrote:
>> It is probably better to move Adhoc_Overloading.thy to
>> ~~/src/HOL/Library and make it import Main. (I am in the process to try
>> this change of Isabelle + AFP.)
> 
> This change (Isabelle/81d90f830f99) broke HOLCF-Prelude in the AFP (see
> attachment).
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.