Skip to content

Commit

Permalink
formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
vzaliva committed Sep 27, 2018
1 parent 9c2c00e commit d2c84b3
Showing 1 changed file with 7 additions and 8 deletions.
15 changes: 7 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -62,12 +62,11 @@ To install all required dependenceis:
This plugin is written using TemplateCoq. After importing you run
template program `mkSwitch` providing the following parameters:

* type (`A`)
* boolean equality predicate on this type (`P: A->A->bool`)
* list of choices `(A * string)` where each element is a tuple of
a constant of type `A` and name of a constructor (as a string).
* name of a new inductive type
* name of selection function
* type (`A`)
* boolean equality predicate on this type (`P: A->A->bool`)
* list of choices `(A * string)` where each element is a tuple of a constant of type `A` and a name of a constructor (as a string).
* name of a new inductive type
* name of selection function

For example, running:

Expand Down Expand Up @@ -117,5 +116,5 @@ Definition Ex1 (n:nat) : T :=

# Contact #

* Repository: https://github.com/vzaliva/coq-switch
* Questions: [Vadim Zaliva](mailto:vzaliva@cmu.edu)
* Repository: https://github.com/vzaliva/coq-switch
* Questions: [Vadim Zaliva](mailto:vzaliva@cmu.edu)

0 comments on commit d2c84b3

Please sign in to comment.