package coq-switch
A plugin to implement functionality similar to `switch` statement in C language
Install
Dune Dependency
Authors
Maintainers
Sources
v1.0.6.tar.gz
md5=8d0fb0ea1951e551e6b598ebab7feac2
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.2.1+8.18" -
coq
>= "8.18.0"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page