package coq-record-update

  1. Overview
  2. Homepage
Generic support for updating record fields in Coq

Install

Dune Dependency

Authors

Maintainers

Sources

v0.3.5.tar.gz
sha512=79f2e8bfff3fd8738b3fea3f39cb16c0d52addcebcb2dd311787dd2061d81c87cb2e65e1388339762e1a643db5cd346bf638181d1ac94a1bdb34ff4884d0f349

Description

While Coq provides projections for each field of a record, it has no convenient way to update a single field of a record. This library provides a generic way to update a field by name, where the user only has to implement a simple typeclass that lists out the record fields.

Dependencies

None

Dev Dependencies (1)

  1. coq (>= "8.14" & < "9.1") | (= "dev")

Conflicts

None

Rocq

Interactive Theorem Prover