package coq-switch
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
A plugin to implement functionality similar to `switch` statement in C language
Install
Dune Dependency
Authors
Maintainers
Sources
v1.0.5.tar.gz
md5=3c9adafc944af4c6472a96212c0a8d73
Description
It allows easier dispatch on several constant values of a type with decidable equality. Given a type, boolean equality predicate, and list of choices, it will generate (using TemplateCoq) an inductive type with constructors, one for each of the choices, and a function mapping values to this type.
Dependencies (2)
-
coq-metacoq-template
>= "1.0~beta2+8.13" -
coq
>= "8.13.0" & < "8.14~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page