format.fmt

%include polycode.fmt
%include greek.fmt
%include forall.fmt


%format failed = "\mathbf{failed}"
%format unknown = "\mathbf{unknown}"
%format free = "\mathbf{free}"

%format <: = "_{"
%format :> = "}\;"
%format </ = "^{"
%format /> = "}\;"
%format :>! = "}"

%format /-> = "\mapsto"
%format ~> = "\Downarrow"
%format ~>* = "\Downarrow ^*"
%format ~>! = "\Downarrow^!"
%format / = "/"
%format ~= = "\; \cong \;"


%format eps = " "
%format .. = "\dots"
%format (vec (a)) = "\overline{" a "}"

%format not = "\Varid{not}"


%format isContext (a) = a "\mbox{~context}"
%format emptycontext = "\emptyset{}"
%format isType (a) = a "\in\mathsf{Type}"
%format isData (a) = a "\in\mathsf{Data}"
%format dataIdx a b = a "\in\mathsf{Data}^{" b "}"
%format emptyset = "\emptyset{}"

%format |- = "\vdash"

%% Format Constructors:
%subst conid a = "\mathsf{" a "}"
%format I = "I"

%format Gamma'

%format alpha_1
%format alpha_2
%format alpha_m
%format alpha_i
%format alpha_l
%format alpha_i_j = alpha "_{i_j}"

%format b_i
%format b_j

%format tau'
%format tau_1
%format tau'_1
%format tau_2
%format tau_n
%format tau'_n
%format tau_i
%format tau'_i
%format tau_l
%format tau_11
%format tau_12
%format tau_1n = tau "_{" 1 n "_{" 1 "}}"
%format tau_21
%format tau_22
%format tau_2n = tau "_{" 2 n "_{" 2 "}}"
%format tau_i
%format tau_i_j = tau "_{i_j}"
%format tau_k_j = tau "_{k_j}"
%format tau_m
%format tau_m1 = tau "_{" m 1 "}"
%format tau_mn = tau "_{" m n "_{" m "}}"
%format tau_im1 = tau "_{" i - 1 "}"

%format rho_1
%format rho_m
%format rho_i

%format x_1
%format x_2
%format x_n
%format x_l
%format x_i
%format x_im1 = x "_{" i - 1 "}"
%format x_i_j = x "_{i_j}"

%format y_1
%format y_2
%format y_n
%format y_l
%format y_i
%format y_nm1 = y "_{" n - 1 "}"

%format z_1
%format z_n

%format e_1
%format e_2
%format e_n
%format e_i

%format n_1
%format n_2

%format p_1
%format p_2
%format p_n

%format C_1
%format C_2
%format C_i
%format C_m
%format C_k

%format Delta'
%format Delta''
%format Delta_0
%format Delta_1
%format Delta_i
%format Delta_n
%format Delta_nm1 = Delta "_{" n - 1 "}"

%format (set (x)) = "\{" x "\}"
%format (Set (ty)) = "\{" ty "\}"
%format (trans (e)) = "\trans{" e "}"
%format (tytrans (ty)) = "\tytrans{" ty "}"

%format <*> = "<\!\!\!*\!\!\!>"
%format <* = "<\!\!\!*"
%format *> = "*\!\!\!>"
%format <$> = "<\!\!\$\!\!>"