Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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'