Julien Puydt (Nov 07 2022 at 11:31): Julien Puydt (Nov 07 2022 at 11:31):Here is an interesting situation:
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section Foo.
Variables a b c: bool.
Check a ==> b ==> c. (* [==> a, b => c]: bool *)
Check ([==> a, b => c]). (* refused: syntax error! *)
End Foo.
so some object gets output in some way, but can't be input like this.
Is it a non-issue? a known issue?
Pierre Roux (Nov 07 2022 at 11:58):Note that [ ==> a, b => c] seems to work. Looks like a bug to me. Note that, since the notation is defined in this file https://github.com/coq/coq/blob/master/theories/ssr/ssrbool.v , if you report/fix the bug, it should be reported/fixed in Coq (not mathcomp).
Paolo Giarrusso (Nov 07 2022 at 12:15):Does the bug still occur if you only import ssrbool.v? Or is it caused by some other import that adds conflicting notations?
Ana de Almeida Borges (Nov 07 2022 at 12:30):Not this case, but I think there can be printing-only notations.
Pierre Roux (Nov 07 2022 at 12:49):Paolo Giarrusso said:
Does the bug still occur if you only import
ssrbool.v? Or is it caused by some other import that adds conflicting notations?
No, same thing with only ssrbool.v imported (and the prelude).
Julien Puydt (Nov 07 2022 at 14:07):Reported here.
Notification Bot (Nov 07 2022 at 14:07):Julien Puydt has marked this topic as resolved.
Pierre Roux (Nov 07 2022 at 16:36):So I don't understand what happens here. If I just try
Local Open Scope bool_scope.
Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0,
format "'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'").
Notation "[ ==> b1 , b2 , .. , bn => c ]" :=
(implb b1 (implb b2 .. (implb bn c) .. )) : bool_scope.
Section Foo.
Variables a b c : bool.
Check [ ==> a, b => c].
Check [==> a, b => c]. (* Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]). *)
whereas
Local Open Scope bool_scope.
Reserved Notation "[==> b1 , b2 , .. , bn => c ]" (at level 0,
format "'[hv' [==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'").
Notation "[ ==> b1 , b2 , .. , bn => c ]" :=
(implb b1 (implb b2 .. (implb bn c) .. )) : bool_scope.
Section Foo.
Variables a b c : bool.
Check [ ==> a, b => c].
Check [==> a, b => c]. (* Error: Unknown interpretation for notation "[==> _ , _ , .. , _ => _ ]". *)
summoning @Hugo Herbelin who is the expert on notations.
Notification Bot (Nov 07 2022 at 16:53):Julien Puydt has marked this topic as unresolved.
Julien Puydt (Nov 07 2022 at 16:56):If the discussion goes on here, I should unmark the topic as closed.
Are those notations actually used enough to warrant having them?
Enrico Tassi (Nov 07 2022 at 19:56):it is probably the [= notation which make this a token and breaks [==> by tokenizing it the wrong way
Pierre Roux (Nov 07 2022 at 20:03):Yes and even if it is not used much (nobody complained until now), it's still a bug. So if it's easy to fix, let's fix it.
Julien Puydt (Nov 08 2022 at 06:06):If those notations are both useless and problematic, why not get rid of them?
Enrico Tassi (Nov 08 2022 at 07:25):yea, the fix seems to be to declare it as [= => for parsing, but I did not try
Pierre Roux (Nov 08 2022 at 10:25):There seems to be a better fix: https://github.com/coq/coq/pull/16788
Last updated: Oct 13 2024 at 01:02 UTC