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.
Set Primitive Projections.
Set Implicit Arguments.
Set Universe Polymorphism.
Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
Inductive Empty :=.
Record category :=
{ ob :> Type;
hom : ob -> ob -> Type
}.
Definition sum_category (C D : category) : category :=
{|
ob := sum (ob C) (ob D);
hom x y := match x, y with
| inl x, inl y => hom x y
| inr x, inr y => hom x y
| _, _ => Empty
end |}.
Goal forall C D (x y : ob (sum_category C D)), Type.
intros C D x y.
hnf in x, y.
exact (hom x y). (* Toplevel input, characters 26-27:
Error:
In environment
C : category
D : category
x : sum (ob C) (ob D)
y : sum (ob C) (ob D)
The term "x" has type "sum (ob C) (ob D)" while it is expected to have type
"ob ?16". *)
Also, it's backwards-incompatible behavior for Set Implicit Arguments.
Also, it's backwards-incompatible behavior for
Set Implicit Arguments
.