Найдите нотацию, которая принимает аргумент инфикс - PullRequest
Новая
       20

Найдите нотацию, которая принимает аргумент инфикс

1 голос
/ 29 октября 2019

В библиотеке Coq.Numbers.Cyclic.ZModulo.ZModulo есть следующие обозначения: 

Notation "[+| c |]" :=
   (interp_carry 1 wB to_Z c) (at level 0, c at level 99).

Как я могу найти это? Я пытался 

Locate "[+| _ |]".  (* Unknown Notation *)
Locate "[+| |]".    (* Unknown Notation *)
Locate "[+| _ |]".  (* Unknown Notation *)
Locate "[+| c |]".  (* Unknown Notation *)
Locate "[+| ?c |]". (* Unknown Notation *)
Locate [+| ?c |].   (* Error: Syntax error: 'Ltac' or [locatable] expected after 'Locate' (in [vernac:command]). *)

1 Ответ

1 голос
/ 29 октября 2019

Ваш первый и четвертый варианты, Locate "[+| _ |]", Locate "[+| c |]". оба верны. Обратите внимание, что имя переменной не имеет значения: вы также можете сделать Locate "[+| abcdef |]"..

Обратите внимание, что конкретная запись, на которую вы ссылаетесь, находится внутри раздела. Это означает , что он недоступен вне раздела. В частности, Locate не найдет его. Чтобы проверить это, попробуйте следующий код: 

Section ZModulo.
  Notation "[+| c |]" := (S c).

  Locate "[+| _ |]".
  (* Notation
     "[+| c |]" := S c (default interpretation) *)

  Locate "[+| c |]".
  (* Notation
     "[+| c |]" := S c (default interpretation) *)

  Locate "[+| abcdef |]".
  (* Notation
     "[+| c |]" := S c (default interpretation) *)
End ZModulo.

Locate "[+| _ |]". (* Unknown notation *)
Locate "[+| c |]". (* Unknown notation *)
Locate "[+| abcdef |]". (* Unknown notation *)

В версиях Coq более ранних, чем 8.8.0, будет работать только первая версия. В 8.8.0 Locate был обновлен , чтобы разрешить другую форму.

...