Add constraints of the form <Occurrence>.<Property> = <Term> to attach metadata to declarations. A d : ty constraint could even be desugared to d.type := ty. We can generate constructors for the labels, and strategies for easy access (e.g. get-type and set-type).

Submitted by Hendrik van Antwerpen on 7 September 2016 at 16:55

Registering properties works, but I need to add some strategies to access them conveniently.

Done, the old types and values for declarations are now unified into properties – although type is builtin, and can be written as d : ty still.