deriving
Inductive type generator
Automatically generates boilerplate code for Coq inductive types
Class instances for Coq inductive types with little boilerplate
24 stars
3 watching
9 forks
Language: Coq
last commit: 3 months ago Related projects:
Repository | Description | Stars |
---|---|---|
| A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
| Provides data structures and reasoning tools for extensional equality in Coq | 29 |
| A plugin for Coq that improves its unification algorithm | 51 |
| Generates type definitions for serialized data formats like JSON | 3 |
| Mechanizations for two dependently-typed languages with graded types | 24 |
| Generates Postman collection and integration tests from Java code | 42 |
| Automates the process of generating TypeScript code from Django models and serializers | 16 |
| Formalizations of compiler design and virtual machine calculations in Coq | 30 |
| A blog about Coq proof assistant and its related libraries and tools | 47 |
| Automates the implementation of IEquatable<T> using attributes. | 138 |
| A tool for generating Coq code from syntactic theories with variable binders | 17 |
| Generates strongly-typed references to controls in Avalonia UI XAML files | 4 |
| Automates formalizing syntactic theories with variable binders in Coq | 52 |
| Automates the generation of strongly typed client code for a GraphQL backend using type-safe wrappers and caching mechanisms. | 154 |