Coq-Equations
Coq-Equations copied to clipboard
mattam82
A function definition package for Coq
The bug can be reproduced by running the file `Attempt1.v` from this [gist](https://gist.github.com/Agnishom/a7414c092c1d23e37afebaa26f57580e#file-attempt1-v) It is not at all clear to me why this bug is happening. However, upon attempting to...
To register the opacity of lemmas generated by equations, the current code, except for issue #83, directly calls `Safe_typing.set_strategy`. This PR synchronizes the occurrences of `Safe_typing.set_strategy` corresponding to the registration...
Hi, When a recursive call in an equation is missing a parameter: ```coq From Equations Require Import Equations. Require Import List Nat. Variant operation := | do_first | do_second. Definition...
~~~coq Require Equations.Prop.Classes. Set Universe Polymorphism. Register Equations.Init.sigma as equations.sigma.type. Register Equations.Init.sigmaI as equations.sigma.intro. Register Equations.Init.pr1 as equations.sigma.pr1. Register Equations.Init.pr2 as equations.sigma.pr2. Register Init.Logic.eq as equations.equality.type. Register Classes.EqDec as equations.eqdec.class....
@coqbot minimize coq-8.16 ```bash #!/usr/bin/env bash opam install -y coq-equations git clone https://github.com/JasonGross/metacoq.git --branch=quotation+typingwf cd metacoq ./configure.sh local make safechecker TIMED=1 -j2 ```
The following Coq file: ``` Require Import Equations.Prop.Equations. Equations Test (a : bool) : bool := Test false := true; Test true := false. Goal (False->False) -> False. simp Test....
```coq Require Import Coq.derive.Derive. Require Equations.Prop.Equations. Derive foo SuchThat (foo = true) as foo_correct. (* Error: Syntax error: [ident] or 'for' expected (in [command]). *) ```
There was a bit of porting involved, but not much. Ideally, it would be nice to get this into opam, I guess it is only a matter of doing a...
Adapt to Coq's new support for algebraic universes everywhere. Also fix the derivation of noconf/noconfhom which introduced unnecessary universes.