aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/names.out
blob: 90ad4ba090748617cee9f154dff4bdad4d6cdb44 (plain)
1
2
3
4
5
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}".