[Scheme Equality] should support let-ins

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

https://coq.inria.fr/

GNU Lesser General Public License v2.1

4.84k stars 647 forks source link

[Scheme Equality] should support let-ins #5287

Open coqbot opened 7 years ago

coqbot commented 7 years ago

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5287 From: @JasonGross Reported version: 8.6 CC: coq-bugs-redist@lists.gforge.inria.fr

See also: BZ#5278

coqbot commented 7 years ago

Comment author: @JasonGross

I would like this to work:

Inductive A' := B' (_ : let T := unit in unit).
Scheme Equality for A'.