Open
Description
(Not sure if this is a JsCoq or coq-lsp issue.)
Consider the following code:
From Coq Require Import Utf8.
Inductive list :=
| nil : list
| cons : nat → list → list.
Notation "[]" := nil.
Notation "n :: ls" := (cons n ls).
Fixpoint concat ls₁ ls₂ :=
match ls₁ with
| [] => ls₂
| x::ls₁' => x::(concat ls₁' ls₂)
end where "ls₁ ++ ls₂" := (concat ls₁ ls₂).
Lemma concat_nil_r : forall ls, ls ++ [] = ls.
Proof.
intros.
induction ls.
- simpl. reflexivity.
- simpl. f_equal. apply IHls.
Qed.The goals displayed by goal view will not correspond to the location of the cursor in the document. Presumably, the reason is that the size of unicode characters is somehow counted wrong.
Metadata
Metadata
Assignees
Labels
No labels