Ошибка синтаксиса с `<` в Coq нотаций

Question

следующий код:

Reserved Notation "g || t |- x < y" (at level 10). 

Inductive SubtypeOf : 
    GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set := 
| SubRefl : 
    forall (gamma : GammaEnv) (theta : ThetaEnv) (u : UnsafeType) , gamma || theta |- u < u 
where "g || t |- x < y" := (SubtypeOf g t x y). 

дает следующее сообщение об ошибке:

Syntax error: '<' expected after [constr:operconstr level 200] (in [constr:operconstr]) 

я получаю подобную ошибку, если я использую <: вместо <.

Но этот код работает отлично:

Reserved Notation "g || t |- x << y" (at level 10). 

Inductive SubtypeOf : 
    GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set := 
| SubRefl : 
    forall (gamma : GammaEnv) (theta : ThetaEnv) (u : UnsafeType) , gamma || theta |- u << u 
where "g || t |- x << y" := (SubtypeOf g t x y). 

Почему? Есть ли параметр приоритета, который можно изменить, чтобы разрешить < или <: в обозначении? Есть ли встроенный синтаксис, с которым я сталкиваюсь, и нужно отслеживать его при определении обозначений?

Answer 1

Coq использует анализатор LL1 для обработки обозначений. Он также может выводить грамматику. Итак, давайте посмотрим, что мы получаем следующие

Reserved Notation "g || t |- x < y" (at level 10). 

Print Grammar constr. выходов:

... 
| "10" LEFTA 
    [ SELF; 
    "||"; 
    constr:operconstr LEVEL "200";  (* subexpression t *) 
    "|-"; 
    constr:operconstr LEVEL "200";  (* subexpression x *) 
    "<"; 
    NEXT 
... 

Здесь

• 10 наш уровень старшинства;
• LEFTA означает левую ассоциативность;
• 200 - уровень приоритета по умолчанию для внутренних подвыражений.

Принимая во внимание тот факт, что более низкий уровень связывает более плотно, чем более высокий уровень, и тот факт, что уровень < составляет 70 (см Coq.Init.Notations), мы можем сделать вывод, что Coq пытается разобрать x < y часть как подвыражение для x, потребляющее токен <, поэтому сообщение об ошибке.

Чтобы исправить ситуацию, мы можем явно запретить разбор третьего параметра как меньшее выражение, назначив более высокий приоритет, т. Е. Более низкий уровень.

Reserved Notation "g || t |- x < y" (at level 10, x at level 69). 

Print Grammar constr. 

| "10" LEFTA 
    [ SELF; 
    "||"; 
    constr:operconstr LEVEL "200";  (* subexpression t *) 
    "|-"; 
    constr:operconstr LEVEL "69";   (* subexpression x *) 
    "<"; 
    NEXT