coq-record-update

Record updater library

Automates creating updaters for individual fields of a record in Coq

Library to create Coq record update functions

GitHub

42 stars
8 watching
16 forks
Language: Coq
last commit: 3 months ago
Linked from 2 awesome lists


Backlinks from these awesome lists:

Related projects:

Repository Description Stars
coq-community/reglang Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant 41
coq-community/coq-tricks A resource for discovering useful techniques and tricks in Coq 503
coq-community/templates Provides template files for generating configuration and boilerplate for Coq projects 13
charguer/tlc A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. 38
tchajed/ltac2-tutorial A tutorial on Ltac2 tactics language for Coq proof scripting 42
coq-community/topology Develops and formalizes basic concepts and results of general topology in Coq. 47
coq-community/bignums A Coq library providing support for arbitrarily large numbers 22
coq-community/parseque A Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq. 42
snu-sf/promising-coq Development of a promising semantics for relaxed-memory concurrency 33
coq-community/coq-art Coq proof assistant book with exercises and examples 110
coq/vscoq A Visual Studio Code extension for Coq proof assistant support 343
coq-community/autosubst Automates formalizing syntactic theories with variable binders in Coq 52
coq-community/coq-ext-lib A collection of reusable Coq definitions and theorems for building software development tools 129
coq-community/chapar A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant 32
coq-community/gaia A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics 28