[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).

Cheers
Lars




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