search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

Indentation issue : "\in" #757

Open KimayaBedarkar opened 7 months ago

KimayaBedarkar commented 7 months ago

SSReflect uses \in as opposed to the unicode ∈ to indicate membership in lists. However, the former is not indented correctly. Example:

Lemma test:
  forall a : nat,
    a \in [::] ->
          False. (* indented by 4 spaces*)

as opposed to:

Lemma test:
  forall a : nat,
    a ∈ [::] ->
    False. (* not indented *)
Matafou commented 2 months ago

Hi. Sadly the coq-smie-user-tokens variable that usually can solve this kind of problem does not work in this case because "\" is not considered as part f a token by PG's lexer. I will think about a way to include this characters in lexing but this will not happen in a short future I am afraid. Sorry...

Poor work around: put parenthesis around a \n [::].

Matafou commented 2 months ago

Actually I think I found a simple way to fix this. @KimayaBedarkar can you test this? I get this indentation now:

Require Import mathcomp.ssreflect.ssrbool.

Definition xx := nat.
Module foo.
  (* from PG issue #757 *)
  Lemma test:
    forall a : nat,
      a \in [::] ->  (* "\in" should be detected as one token *)
      False.
  Proof.
  Abort.

  Lemma test2:
    forall a : nat,
      a \in  (* "\in" should be detected as one token *)
        [::] ->
      False.
End foo.