package coq-record-update

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

Install

Dune Dependency

Authors

Maintainers

Sources

v0.3.6.tar.gz
sha512=d5f051a5fe89ba518f9b1caae5d5e014bc7af1294d46d9f3bf01527f5a124122e0e7a4e46c575060dd21ca5b9fc1c0f3a50535397869f2ac93f5518dee8c06b9

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