
%format fst     = "\pi_1 "
%format snd     = "\pi_2 "

%format Either x y = x "+ " y
%format Left    = "\iota_L "
%format Right   = "\iota_R "

%format Mu      = "\mu "
%format InF	    = "in "
%format outF	= "out "

%format cata x = "\llparenthesis "  x  "\rrparenthesis "
%format ana x  = "[\!( " x ")\!]"

%format Inl     = "\kappa_L "
%format Inr     = "\kappa_R "


%format undefined = "\bot "
%format bot = "\bot "


%format °   = "\bullet "
%format ./\.    = "\sqcap "
%format .\/.    = "\sqcup "


%format <*>   = "\times "
%format :*:   = "\times "
%format /\    = "\times "
%format prod p q = "\langle" p "," q "\rangle"


%format <|> = "+ "
%format :+: = "+ "
%format \/  = "+ "
%format coprod p q = "[" p "," q "]"


%format eval x = "\llbracket " x "\rrbracket "


%format Bool      = "\BB "
%format True      = "\true "
%format False     = "\false "
%format not      = "\neg "
%format ||       = "\vee "
%format &&       = "\wedge "
%format ==       = "\equiv "


%format elem = "(\in) "
%format `elem` = "\in "
%format `isSubsetOf` = "\subseteq "
%format `intersection` = "\cap "
%format length x = "|" x "|"



%format return = "\eta "

%format Maybe a = a "_\nabla "
%format Just = "\eta "
%format Nothing = "\nabla "

%format Integer = "\NN"
%format Int = "\NN "
%format Nat = "\NN "


%format delta   = "\delta "
%format phi     = "\phi "
%format rho     = "\rho "
%format lambda  = "\lambda "
%format alpha  = "\alpha "
%format beta  = "\beta "
%format sigma  = "\sigma "

%format delta'
%format phi'
%format rho'
%format lambda'
%format alpha'
%format beta'
%format sigma'


%format tr  = "\sigma "
%format mo  = "\mode "
%format st  = "S "
%format keepFrom i s = s "^{" i "}"


%format LangF x = "{\mathsf{L}}_ " x
%format Lang x = "{\Lang}_ " x
%format denotP x = "\llbracket" x "\rrbracket_P"
%format denotD x = "\llbracket" x "\rrbracket_D"
%format denotC x = "\llbracket" x "\rrbracket_C"
%format denotE x = "\llbracket" x "\rrbracket_E"
%format denotAt ev x = "\llbracket" x "\rrbracket_{ev}"
%format denotL ev x = "\llbracket" x "\rrbracket_\Lang\; " ev 
%format denot x = "\llbracket" x "\rrbracket"


%format Subs    = "\Sigma "
%format Prop    = "P "
%format Event   = "E "

%format Mode    = "\mode "
%format Obl     = "\obl "
%format For     = "\for "
%format swapMode m  = m "^\dagger "


%format Dead    = "(\dead) "
%format `Dead`  = "\dead "
%format None    = "(\emptyset) "
%format Always  = "(\top) "
%format Inj     = "(\iota_R) "
%format `Inj`   = "\iota_R "

%format Atom    = "\iota "
%format atom    = "\iota "


%format Trig    = "(\trig) "
%format `Trig`  = "\trig "
%format `trig`  = "\trig "
%format Trug    = "(\trug) "
%format `Trug`  = "\trug "
%format `trug`  = "\trug "
%format Conj    = "(\conj) "
%format `Conj`  = "\conj "
%format `conj`  = "\conj "
%format Sanc    = "(\sanc) "
%format `Sanc`  = "\sanc "
%format `sanc`  = "\sanc "



%format TNot    = "\neg "
%format TSum    = "(+) "
%format `TSum`  = "+ "
%format TLeq    = "(\leq) "
%format `TLeq`  = "\leq "
%format TEq    = "(\equiv) "
%format `TEq`  = "\equiv "
%format TElem   = "(\in) "
%format `TElem` = "\in "
%format THead   = "(\succcurlyeq) "
%format `THead` = "\succcurlyeq "
%format headOf   = "\succcurlyeq "
%format TPrice = "\text{price} "




%format LTL     = "\LLTL "

%format P x       = x
%format Wedge     = "(\wedge) "
%format Vee       = "(\vee) "
%format Imply     = "(\imp) "
%format `Wedge`     = "\wedge "
%format `Vee`       = "\vee "
%format `Imply`     = "\imp "
%format Not         = "\neg "
%format Diamond     = "\always "
%format Lozenge     = "\hence "
%format Until       = "(\until) "
%format Weak        = "(\weak) "
%format `Until`     = "\until "
%format `Weak`      = "\weak "
%format Next        = "\nex "

%format lP x       = x
%format (lP x)     = x
%format lWedge     = "(\wedge) "
%format lVee       = "(\vee) "
%format lImply     = "(\imp) "
%format `lWedge`     = "\wedge "
%format `lVee`       = "\vee "
%format `lImply`     = "\imp "
%format lNot         = "\neg "
%format lDiamond     = "\always "
%format lLozenge     = "\hence "
%format lUntil       = "(\until) "
%format lWeak        = "(\weak) "
%format `lUntil`     = "\until "
%format `lWeak`      = "\weak "
%format lNext        = "\nex "



