Anomaly: not an arity. Please report. (polyproj)

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

Anomaly: not an arity. Please report. (polyproj) #115

Open JasonGross opened 10 years ago

JasonGross commented 10 years ago

Inductive T : let U := Type in U := t. (* Anomaly: not an arity. Please report. *)

This works in trunk, but not in trunk-polyproj.