Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use Defined for EqDec instances instead of Qed #24

Open
jbaum98 opened this issue Oct 11, 2018 · 1 comment
Open

Use Defined for EqDec instances instead of Qed #24

jbaum98 opened this issue Oct 11, 2018 · 1 comment

Comments

@jbaum98
Copy link

jbaum98 commented Oct 11, 2018

As described in PrincetonUniversity/VST#290, the use of Qed when creating typeclass instances makes it so that you can't evaluate expressions using the typeclass:

Compute 1 ?= 1.
     = (let (eqb, _) := nat_EqDec in eqb) 1 1

The instances in EqDec.v that currently end in Qed and shoulde be changed to Defined are:

  • Vector_EqDec
  • unit_EqDec
  • bool_EqDec
  • nat_EqDec
  • option_EqDec
  • list_EqDec
@adampetcher
Copy link
Owner

This is likely a good idea, but making definitions transparent tends to cause problems when they are used. At least, it used to cause problems in older versions of Coq. Can you produce a pull request so I can see how well this works in Coq 8.8?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants