[isabelle] Faux record update syntax
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Faux record update syntax
- From: Lars Hupel <hupel at in.tum.de>
- Date: Tue, 28 Mar 2017 18:16:41 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0
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