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". *)
|
