coq-record-update icon indicating copy to clipboard operation
coq-record-update copied to clipboard

Add some Ltac to autogenerate Settable

Open JasonGross opened this issue 4 years ago • 0 comments

Note that field-setting is up to unification, and so we fully normalize the type of the record when generating the instance. This will be very slow for large record types. Finally, the term generated by setting a field will use unfolded projections, which may be more ugly. The combination of these suggests that you may not want to include this, or you may want to make this optional.

JasonGross avatar Jan 19 '21 18:01 JasonGross