summaryrefslogtreecommitdiff
path: root/test-suite/output/names.out
blob: 2892dfd5a1a45fa06853da930f3a310fd4147d6a (plain)
1
2
3
4
5
6
The command has indeed failed with message:
=> Error:
In environment
y : nat
The term "a y" has type "{y0 : nat | y = y0}"
while it is expected to have type "{x : nat | x = y}".