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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and