snyke7
snyke7
I just ran into this when testing my code for 8.19. I believe the Ltac2 version of `List.fold_right2` and `List.fold_left2` still have the 'wrong' order, i.e. do not match the...
I would also appreciate a conversion function for integers, `to_int : Ltac1.t -> int option`.
I have a tactic `iStep`, and another `Tactic Notation "iStep" integer(n) := ...` (so exposed in Ltac1), which behaves like `do n iStep.` but is more efficient. The implementation itself...
> This is definitely forbidden knowledge... 😳️ > Does the Ltac1 tactic notation with an integer works with a variable already? I think there is some partial support for it...
EDIT: I made a typo, see my earlier post --------------------- But anyway, I hope my earlier example has demonstrated an appropriate use case for the `to_int : Ltac1.t -> int...
Woops, indeed, edited my posts.
I usually get the horrible looking error messages when setoid rewriting fails. Here is a smallish example: ``` From Coq Require Import Relations Setoid. Class LeftId {A} (R : relation...