There is some kind of parsing issue with the command when it takes a Notation as argument.
From the test suite:
Lemma lem_lelst_sorted {A} {dto : DecTotalOrder A} :
forall l x, Sorted (x :: l) <-> LeLst x l /\ Sorted l.
Proof.
induction l; sauto l: on use: lem_lelst_trans inv: Sorted, List.Forall ctrs: Sorted.
Qed.
Fails with error:
Error: not an inductive type: List.Forall
The problem is apparently that Stdlib.Lists.List defines:
Notation Forall := Forall.
(maybe to improve reverse compatibility later on if they ever redefine Forall?)
and so the actual inductive type is being hidden by the notation List.Forall.
The example in the test suite is easy to fix (changing List.Forall to Forall) but is there a way to change the parsing grammar to be more robust to this kind of thing so it understands that a notation for an inductive type should be treated as an inductive type?)
There is some kind of parsing issue with the command when it takes a
Notationas argument.From the test suite:
Fails with error:
The problem is apparently that
Stdlib.Lists.Listdefines:(maybe to improve reverse compatibility later on if they ever redefine
Forall?)and so the actual inductive type is being hidden by the notation
List.Forall.The example in the test suite is easy to fix (changing
List.ForalltoForall) but is there a way to change the parsing grammar to be more robust to this kind of thing so it understands that a notation for an inductive type should be treated as an inductive type?)