Re: [isabelle] Faux record update syntax



On 28/03/17 18:16, Lars Hupel wrote:
> 
> I stumbled over a funny thing today: Even if a value x is not of record
> type, record update syntax will still work. For example,
> 
>   x (| v := t |)
> 
> works as long as a constant v_update with the appropriate type is in scope.

This was done on purpose many years ago, when this notation was
introduced. A bit later, the record package turned out the canonical
source of such update functions, but there are (very few) other
applications found elsewhere.


	Makarius






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