coq-switch

A plugin to implement functionality similar to `switch` statement in C language. 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.

opam install coq-switch.1.0.0
homepage
https://github.com/vzaliva/coq-switch
license
MIT
bugs tracker
https://github.com/vzaliva/coq-switch/issues
dependencies
coq >= 8.8 & coq-template-coq >= 2.1~beta3
source
https://github.com/vzaliva/coq-switch/archive/v1.0.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-switch/coq-switch.1.0.0