[isabelle] Faux record update syntax

Dear list,

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.

Should the datatype command be extended to produce these constants? It
is quite convenient syntax (which can't be said of records in general).


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