aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_041.v
blob: 79933bb854bcf48ac09b8db2d5ff149a92194ba4 (plain)
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"). *)