blob: 6e66a6a90a2a36e8978c53ef940d81719f2543b5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Inductive any_list {A} :=
| nil : @any_list A
| cons : forall X, A -> @any_list X -> @any_list A.
Arguments nil {A}.
Arguments cons {A X}.
Notation "[]" := (@nil Type).
Notation "hd :: tl" := (cons hd tl).
Definition xs := true :: 2137 :: false :: 0 :: [].
Fail Definition ys := xs :: xs.
(* Goal ys = ys. produced an anomaly "Unable to handle arbitrary u+k <= v constraints" *)
|
