1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Set Printing All.
Definition foo (s d : Prop)
: ((s : Set) -> (d : Set)) = ((s : Prop) -> (d : Prop))
:= eq_refl. (* succeeds *)
Definition bar (s d : Prop)
: ((fun x : Set => x) s -> (fun x : Set => x) d) = ((fun x : Prop => x) s -> (fun x : Prop => x) d)
:= eq_refl. (* Toplevel input, characters 131-138:
Error:
In environment
s : Prop
d : Prop
The term
"@eq_refl Set (forall _ : (fun x : Set => x) s, (fun x : Set => x) d)"
has type "@eq Set (forall _ : s, d) (forall _ : s, d)"
while it is expected to have type
"@eq Set (forall _ : s, d) (forall _ : s, d)"
(cannot unify "forall _ : (fun x : Set => x) s, (fun x : Set => x) d" and
"forall _ : (fun x : Prop => x) s, (fun x : Prop => x) d"). *)
|
