aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_037.v
blob: 66476414671a8555b1e0405d21f238e8ab0a3105 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Set Printing Universes.

Fixpoint CardinalityRepresentative (n : nat) : Set :=
  match n with
    | O => Empty_set
    | S n' => sum (CardinalityRepresentative n') unit
  end.
(* Toplevel input, characters 104-143:
Error:
In environment
CardinalityRepresentative : nat -> Set
n : nat
n' : nat
The term "(CardinalityRepresentative n' + unit)%type" has type
 "Type (* max(Top.73, Top.74) *)" while it is expected to have type
"Set". *)