Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/7c1115328046ba56778348d68efe410e]
typ : type.
=> : typ -> typ -> typ.
%infix right 8 =>.
& : typ -> typ -> typ.
%infix none 9 &.
unit : typ.
exp : type.
val : type.
value : val -> exp.
lam : (val -> exp) -> val.
app : exp -> exp -> exp.
mkpair : exp -> exp -> exp.
pair : val -> val -> val.
fst : exp -> exp.
snd : exp -> exp.
1 : val.
let : exp -> (val -> exp) -> exp.
of : exp -> typ -> type.
ofv : val -> typ -> type.
ofvalue : {V:val} {A:typ} ofv V A -> of (value V) A.
unitI : ofv 1 unit.
=>I :
   {A:typ} {M:val -> exp} {B:typ}
      ({x:val} ofv x A -> of (M x) B) -> ofv (lam ([x:val] M x)) (A => B).
=>E :
   {M1:exp} {A:typ} {B:typ} {M2:exp}
      of M1 (A => B) -> of M2 A -> of (app M1 M2) B.
&Iv :
   {V1:val} {A:typ} {V2:val} {B:typ}
      ofv V1 A -> ofv V2 B -> ofv (pair V1 V2) (A & B).
&I :
   {M1:exp} {A:typ} {M2:exp} {B:typ}
      of M1 A -> of M2 B -> of (mkpair M1 M2) (A & B).
&E1 : {M:exp} {A:typ} {B:typ} of M (A & B) -> of (fst M) A.
&E2 : {M:exp} {A:typ} {B:typ} of M (A & B) -> of (snd M) B.
oflet :
   {M:exp} {A:typ} {N:val -> exp} {C:typ}
      of M A -> ({y:val} ofv y A -> of (N y) C) -> of (let M ([x:val] N x)) C.
cexp : type.
ctyp : type.
cval : type.
ccont : ctyp -> ctyp.
%postfix 8 ccont.
c& : ctyp -> ctyp -> ctyp.
%infix none 9 c&.
cunit : ctyp.
cmkpair : cval -> cval -> (cval -> cexp) -> cexp.
cfst : cval -> (cval -> cexp) -> cexp.
csnd : cval -> (cval -> cexp) -> cexp.
ccall : cval -> cval -> cexp.
chalt : cexp.
cpair : cval -> cval -> cval.
clam : (cval -> cexp) -> cval.
c1 : cval.
cof : cexp -> type.
%mode *{C:cexp} (cof C).
cofv : cval -> ctyp -> type.
%mode *{A:cval} *{B:ctyp} (cofv A B).
co_halt : cof chalt.
co_mkpair :
   {V1:cval} {A:ctyp} {V2:cval} {B:ctyp} {K:cval -> cexp}
      cofv V1 A -> cofv V2 B -> ({v:cval} cofv v (A c& B) -> cof (K v))
         -> cof (cmkpair V1 V2 ([v:cval] K v)).
co_call :
   {F:cval} {A:ctyp} {V:cval} cofv F (A ccont) -> cofv V A -> cof (ccall F V).
co_fst :
   {V:cval} {A:ctyp} {B:ctyp} {C:cval -> cexp}
      cofv V (A c& B) -> ({v:cval} cofv v A -> cof (C v))
         -> cof (cfst V ([v:cval] C v)).
co_snd :
   {V:cval} {A:ctyp} {B:ctyp} {C:cval -> cexp}
      cofv V (A c& B) -> ({v:cval} cofv v B -> cof (C v))
         -> cof (csnd V ([v:cval] C v)).
cov_unit : cofv c1 cunit.
cov_pair :
   {V1:cval} {A:ctyp} {V2:cval} {B:ctyp}
      cofv V1 A -> cofv V2 B -> cofv (cpair V1 V2) (A c& B).
cov_lam :
   {A:ctyp} {C:cval -> cexp}
      ({x:cval} cofv x A -> cof (C x)) -> cofv (clam ([v:cval] C v)) (A ccont).
ttoct : typ -> ctyp -> type.
%mode +{A:typ} -{CA:ctyp} (ttoct A CA).
ttoct/unit : ttoct unit cunit.
ttoct/& :
   {A:typ} {A':ctyp} {B:typ} {B':ctyp}
      ttoct A A' -> ttoct B B' -> ttoct (A & B) (A' c& B').
ttoct/=> :
   {A:typ} {A':ctyp} {B:typ} {B':ctyp}
      ttoct A A' -> ttoct B B' -> ttoct (A => B) (A' c& (B' ccont) ccont).
%worlds () (ttoct _ _).
%total D (ttoct D _).
tocpsv+ :
   {V:val} {A:typ} {CA:ctyp} {CV:cval}
      ofv V A -> ttoct A CA -> cofv CV CA -> type.
%mode +{V:val} +{A:typ} +{CA:ctyp} -{CV:cval} +{WV:ofv V A} +{CT:ttoct A CA}
   -{WCV:cofv CV CA} (tocpsv+ WV CT WCV).
tocpsv- :
   {V:val} {A:typ} {CA:ctyp} {CV:cval}
      ofv V A -> ttoct A CA -> cofv CV CA -> type.
%mode +{V:val} +{A:typ} -{CA:ctyp} -{CV:cval} +{WV:ofv V A} -{CT:ttoct A CA}
   -{WCV:cofv CV CA} (tocpsv- WV CT WCV).
tocps- :
   {A:typ} {CA:ctyp} {M:exp}
      of M A -> ttoct A CA
         -> ({CC:(cval -> cexp) -> cexp}
                ({C:cval -> cexp}
                    ({cv:cval} cofv cv CA -> cof (C cv))
                       -> cof (CC ([v:cval] C v))) -> type).
%mode +{A:typ} -{CA:ctyp} +{M:exp} +{WM:of M A} -{CT:ttoct A CA}
   -{CC:(cval -> cexp) -> cexp}
   -{WCC:{C:cval -> cexp}
            ({cv:cval} cofv cv CA -> cof (C cv)) -> cof (CC ([v:cval] C v))}
   (tocps- M WM CT CC WCC).
[Closing file /home/www/twelfwiki/code/7c1115328046ba56778348d68efe410e]
/home/www/twelfwiki/code/7c1115328046ba56778348d68efe410e:167.1-167.2 Error: 
Expected constant name or pragma keyword, found `['
%% ABORT %%