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

Stack overflow on "Hint Rewrite @<primitive projection>" (polyproj) #122

Open JasonGross opened 10 years ago

JasonGross commented 10 years ago 
(* File reduced by coq-bug-finder from original input, then from 669 lines to 79 lines, then from 89 lines to 44 lines *)
Set Primitive Projections.
Reserved Notation "g 'o' f" (at level 40, left associativity).
Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Notation "x = y" := (@paths _ x y) : type_scope.

Set Implicit Arguments.

Record PreCategory :=
  Build_PreCategory' {
      object :> Type;
      morphism : object -> object -> Type;

      identity : forall x, morphism x x;
      compose : forall s d d',
                  morphism d d'
                  -> morphism s d
                  -> morphism s d'
                              where "f 'o' g" := (compose f g);

      left_identity : forall a b (f : morphism a b), identity b o f = f
    }.

Hint Rewrite @left_identity. (* stack overflow *)