tchajed/coq-record-update

This is stars and forks stats for /tchajed/coq-record-update repository. As of 26 Apr, 2024 this repository has 40 stars and 14 forks.

Coq record update library In a nutshell, this library automatically provides a generic way to update record fields. Here's a teaser example: From RecordUpdate Require Import RecordSet. Record X := mkX { A: nat; B: nat; C: bool; }. (* all you need to do is provide something like this, listing out the fields of your record: *) #[export] Instance etaX : Settable _ := settable! mkX <A; B; C>. (* and now you can update fields! *) Definition setAB a b x := set B b (set A a x). (* you can also use...