aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/names.out
blob: 48be63a46ab852b2f537ed388feec326e14bca30 (plain)
1
2
3
4
5
6
7
8
9
10
11
The command has indeed failed with message:
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}".
1 focused subgoal
(shelved: 1)
  
  H : ?n <= 3 -> 3 <= ?n -> ?n = 3
  ============================
  True