metavar termvar, x ::=   {{ com  term variable }} 
{{ isa string}} {{ coq nat}} {{ hol string}} {{ coq-equality }}
{{ ocaml int}} {{ lex alphanum}} {{ tex \mathit{[[termvar]]} }}

grammar
t :: 't_' ::=                               {{ com term    }}
  | x            ::  :: Var                   {{ com variable}}
  | \ x . t      ::  :: Lam (+ bind x in t +) {{ com lambda  }}
  | t t'         ::  :: App                   {{ com app     }}
  | ( t )        :: S:: Paren                 {{ icho [[t]]  }} 
  | { t / x } t' :: M:: Tsub  
                        {{ icho (tsubst_t [[t]] [[x]] [[t']])}}

v :: 'v_' ::=                               {{ com value   }}
  | \ x . t      ::  :: Lam                   {{ com lambda  }}

terminals :: 'terminals_' ::=
  | \            ::  :: lambda  {{ tex \lambda }}
  | -->          ::  :: red     {{ tex \longrightarrow }}

subrules
  v <:: t

substitutions
  single t x :: tsubst 

defns
Jop :: '' ::=

 defn
 t1 --> t2 :: ::reduce::'' {{ com $[[t1]]$ reduces to $[[t2]]$}} by


    --------------------------  :: ax_app
    (\x.t12) v2 -->  {v2/x}t12

    t1 --> t1'
    -------------- :: ctx_app_fun
    t1 t --> t1' t

    t1 --> t1'
    -------------- :: ctx_app_arg
    v t1 --> v t1'

This document was translated from L^AT_EX by H^EV^EA.