search

HoTT / 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.
http://coq.inria.fr/
GNU Lesser General Public License v2.1
27 stars 5 forks source link

trunk-polyproj seems to be missing eta for records? (polyproj) #104

Closed JasonGross closed 10 years ago

JasonGross commented 10 years ago 
Set Implicit Arguments.

Require Import Logic.

Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.
Local Set Record Elimination Schemes.
Local Set Primitive Projections.

Record prod (A B : Type) : Type :=
  pair { fst : A; snd : B }.

Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x).

fails. Has eta for records been removed from trunk-polyproj? Is it still slated for 8.5?

JasonGross commented 10 years ago

Oops, I re-reported a more accurate version as #124. Closing this one.