package coq-record-update
  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.
Tags
category:Computer Science/Data Types and Data Structures keyword:record logpath:RecordUpdate date:2025-09-05Published: 08 Sep 2025
Dependencies
None
Dev Dependencies (1)
- 
  
    coq
  
  
    (>= "8.14" & < "9.2") | (= "dev")
Used by (2)
Conflicts
None
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
On This Page