baddCoqOtt.ott

% !Ott args = "-coq_expand_list_types=false -o minirust.tex -o minirust.v"


metavar typvar, X ::=
   {{ coq nat }} {{ coq-equality }}

indexvar n ::=  {{ coq nat }}

grammar


Kind, K :: kind_ ::= {{ coq-equality  }}
  | KindStar :: :: KindStar 
 

typexpr, T :: T_ ::=    {{ coq-equality }}                   
    | X                   ::   :: var                     
    | ForAll << X1 , .. , Xn >> .  T            ::   :: polyarrow
    |  [ X1 |-> tau1 .. Xn |-> taun ] T        :: M :: tsub  {{ coq (tsubst_typexpr [[X1 |-> tau1 .. Xn |-> taun]] [[T]]) }}


tau :: tau_ ::=    
    | X                   ::   :: var   
    

grammar

    formula :: 'formula_' ::=
      | judgement           ::   :: judgement
      | formula1 .. formulan :: :: dots


    subrules
      tau <:: T

    substitutions
      multiple typexpr X  :: tsubst 
      

    defns
      Jtype :: '' ::=



    defn
        |- T : K :: :: kind :: Kind by
       
        ------------------------------------ :: Var
        |- T : KindStar

        
       
    defn
        |- T <: T' :: :: sub :: Sub by
 

        </ |-  taun : KindStar // n />
        ------------------------------------------ :: InstL
        |-  ForAll << </ Xn // n /> >> .  T  <: [ </ Xn |-> taun // n /> ] T