% !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