The time is now Saturday, October 3rd, 2015 6:11:41am /usr/bin/ssh -R 18333:localhost:18333 racket@192.168.56.108 '/usr/bin/env' 'DISPLAY=:1' 'PLT_PKG_BUILD_SERVICE=1' 'PLTUSERHOME=/home/racket/build-pkgs/user' '/bin/sh' '-c' 'cd "/home/racket/build-pkgs"/racket && bin/raco pkg install -u --auto cur' Resolving "cur" via http://localhost:18333/built/catalog/ Resolving "cur" via http://localhost:18333/archive/catalog/ Downloading http://localhost:18333/archive/pkgs/cur.zip raco setup: version: 6.2 [3m] raco setup: installation name: 6.2 raco setup: variants: 3m raco setup: main collects: /home/racket/build-pkgs/racket/collects raco setup: collects paths: raco setup: /home/racket/build-pkgs/user/.racket/6.2/collects raco setup: /home/racket/build-pkgs/racket/collects raco setup: main pkgs: /home/racket/build-pkgs/racket/share/pkgs raco setup: pkgs paths: raco setup: /home/racket/build-pkgs/racket/share/pkgs raco setup: /home/racket/build-pkgs/user/.racket/6.2/pkgs raco setup: links files: raco setup: /home/racket/build-pkgs/racket/share/links.rktd raco setup: /home/racket/build-pkgs/user/.racket/6.2/links.rktd raco setup: main docs: /home/racket/build-pkgs/racket/doc raco setup: --- updating info-domain tables --- raco setup: updating: /home/racket/build-pkgs/user/.racket/6.2/share/info-cache.rktd raco setup: --- pre-installing collections --- raco setup: --- installing foreign libraries --- raco setup: --- installing shared files --- raco setup: --- compiling collections --- raco setup: making: /cur raco setup: in /cur raco setup: in /cur/curnel raco setup: in /cur/stdlib raco setup: in /cur/scribblings raco setup: in /cur/scribblings/stdlib raco setup: making: /cur/curnel raco setup: making: /cur/examples raco setup: in /cur/examples raco setup: in /cur/stdlib Church-Rosser broken (((((((((((((((((((((∅ (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Var : (Unv 0) ((avar : (Π (g5263 : Nat) Var))))) (Maybe : (Π (A : (Unv 0)) (Unv 0)) ((none : (Π (A : (Unv 0)) (Maybe A))) (some : (Π (A : (Unv 0)) (Π (a : A) (Maybe A))))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (True : (Unv 0) ((T : True)))) (False : (Unv 0) ())) (And : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : A) (Π (y : B) ((And A) B))))))))) (== : (Π (A : (Unv 0)) (Π (x : A) (Π (g6949 : A) (Unv 0)))) ((refl : (Π (A : (Unv 0)) (Π (x : A) (((== A) x) x))))))) (stlc-val : (Unv 0) ((stlc-true : stlc-val) (stlc-false : stlc-val) (stlc-unit : stlc-val)))) (stlc-type : (Unv 0) ((stlc-boolty : stlc-type) (stlc-unitty : stlc-type) (stlc--> : (Π (g7411 : stlc-type) (Π (g7412 : stlc-type) stlc-type))) (stlc-* : (Π (g7413 : stlc-type) (Π (g7414 : stlc-type) stlc-type)))))) (stlc-term : (Unv 0) ((Var-->-stlc-term : (Π (g7415 : Var) stlc-term)) (stlc-val-->-stlc-term : (Π (g7416 : stlc-val) stlc-term)) (stlc-app : (Π (g7417 : stlc-term) (Π (g7418 : stlc-term) stlc-term))) (stlc-lambda : (Π (g7419 : Var) (Π (g7420 : stlc-type) (Π (g7421 : stlc-term) stlc-term)))) (stlc-cons : (Π (g7422 : stlc-term) (Π (g7423 : stlc-term) stlc-term))) (stlc-let : (Π (g7424 : Var) (Π (g7425 : Var) (Π (g7426 : stlc-term) (Π (g7427 : stlc-term) stlc-term)))))))) (Gamma : (Unv 0) ((emp-gamma : Gamma) (extend-gamma : (Π (g7428 : Gamma) (Π (g7429 : Var) (Π (g7430 : stlc-type) Gamma))))))) (Π (g2 : (Maybe stlc-type)) (Unv 0))) ((((((((((((((((((((∅ (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Var : (Unv 0) ((avar : (Π (g5263 : Nat) Var))))) (Maybe : (Π (A : (Unv 0)) (Unv 0)) ((none : (Π (A : (Unv 0)) (Maybe A))) (some : (Π (A : (Unv 0)) (Π (a : A) (Maybe A))))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (True : (Unv 0) ((T : True)))) (False : (Unv 0) ())) (And : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : A) (Π (y : B) ((And A) B))))))))) (== : (Π (A : (Unv 0)) (Π (x : A) (Π (g6949 : A) (Unv 0)))) ((refl : (Π (A : (Unv 0)) (Π (x : A) (((== A) x) x))))))) (stlc-val : (Unv 0) ((stlc-true : stlc-val) (stlc-false : stlc-val) (stlc-unit : stlc-val)))) (stlc-type : (Unv 0) ((stlc-boolty : stlc-type) (stlc-unitty : stlc-type) (stlc--> : (Π (g7411 : stlc-type) (Π (g7412 : stlc-type) stlc-type))) (stlc-* : (Π (g7413 : stlc-type) (Π (g7414 : stlc-type) stlc-type)))))) (stlc-term : (Unv 0) ((Var-->-stlc-term : (Π (g7415 : Var) stlc-term)) (stlc-val-->-stlc-term : (Π (g7416 : stlc-val) stlc-term)) (stlc-app : (Π (g7417 : stlc-term) (Π (g7418 : stlc-term) stlc-term))) (stlc-lambda : (Π (g7419 : Var) (Π (g7420 : stlc-type) (Π (g7421 : stlc-term) stlc-term)))) (stlc-cons : (Π (g7422 : stlc-term) (Π (g7423 : stlc-term) stlc-term))) (stlc-let : (Π (g7424 : Var) (Π (g7425 : Var) (Π (g7426 : stlc-term) (Π (g7427 : stlc-term) stlc-term)))))))) (Gamma : (Unv 0) ((emp-gamma : Gamma) (extend-gamma : (Π (g7428 : Gamma) (Π (g7429 : Var) (Π (g7430 : stlc-type) Gamma))))))) (Π (g3 : (Maybe stlc-type)) (Unv 0))) ((((((((((((((((((((∅ (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Var : (Unv 0) ((avar : (Π (g5263 : Nat) Var))))) (Maybe : (Π (A : (Unv 0)) (Unv 0)) ((none : (Π (A : (Unv 0)) (Maybe A))) (some : (Π (A : (Unv 0)) (Π (a : A) (Maybe A))))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (True : (Unv 0) ((T : True)))) (False : (Unv 0) ())) (And : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : A) (Π (y : B) ((And A) B))))))))) (== : (Π (A : (Unv 0)) (Π (x : A) (Π (g6949 : A) (Unv 0)))) ((refl : (Π (A : (Unv 0)) (Π (x : A) (((== A) x) x))))))) (stlc-val : (Unv 0) ((stlc-true : stlc-val) (stlc-false : stlc-val) (stlc-unit : stlc-val)))) (stlc-type : (Unv 0) ((stlc-boolty : stlc-type) (stlc-unitty : stlc-type) (stlc--> : (Π (g7411 : stlc-type) (Π (g7412 : stlc-type) stlc-type))) (stlc-* : (Π (g7413 : stlc-type) (Π (g7414 : stlc-type) stlc-type)))))) (stlc-term : (Unv 0) ((Var-->-stlc-term : (Π (g7415 : Var) stlc-term)) (stlc-val-->-stlc-term : (Π (g7416 : stlc-val) stlc-term)) (stlc-app : (Π (g7417 : stlc-term) (Π (g7418 : stlc-term) stlc-term))) (stlc-lambda : (Π (g7419 : Var) (Π (g7420 : stlc-type) (Π (g7421 : stlc-term) stlc-term)))) (stlc-cons : (Π (g7422 : stlc-term) (Π (g7423 : stlc-term) stlc-term))) (stlc-let : (Π (g7424 : Var) (Π (g7425 : Var) (Π (g7426 : stlc-term) (Π (g7427 : stlc-term) stlc-term)))))))) (Gamma : (Unv 0) ((emp-gamma : Gamma) (extend-gamma : (Π (g7428 : Gamma) (Π (g7429 : Var) (Π (g7430 : stlc-type) Gamma))))))) (Π (g4 : (Maybe stlc-type)) (Unv 0)))) compilation context...: /home/racket/build-pkgs/user/.racket/6.2/pkgs/cur/examples/stlc.rkt context...: /home/racket/build-pkgs/racket/collects/racket/private/map.rkt:21:13: map /home/racket/build-pkgs/racket/share/pkgs/redex-lib/redex/private/reduction-semantics.rkt:1702:23: loop /home/racket/build-pkgs/racket/share/pkgs/redex-lib/redex/private/judgment-form.rkt:298:10: for-loop /home/racket/build-pkgs/racket/share/pkgs/redex-lib/redex/private/judgment-form.rkt:287:0: judgment-form-bind-withs/proc /home/racket/build-pkgs/racket/share/pkgs/redex-lib/redex/private/judgment-form.rkt:298:10: for-loop /home/racket/build-pkgs/racket/share/pkgs/redex-lib/redex/private/judgment-form.rkt:287:0: judgment-form-bind-withs/proc /home/racket/build-pkgs/racket/share/pkgs/redex-lib/redex/private/judgment-form.rkt:991:0: combine-judgment-rhses /home/racket/build-pkgs/racket/collects/racket/private/more-scheme.rkt:370:13: hash-ref! /home/racket/build-pkgs/racket/collects/racket/private/more-scheme.rkt:370:13: hash-ref! /home/racket/build-pkgs/racket/collects/racket/private/more-scheme.rkt:370:13: hash-ref! /home/racket/build-pkgs/racket/collects/racket/private/more-scheme.rkt:370:13: hash-ref! /home/racket/build-pkgs/racket/collects/racket/private/more-scheme.rkt:370:13: hash-ref! /home/racket/build-pkgs/racket/collects/racket/private/more-scheme.rkt:370:13: hash-ref! /home/racket/build-pkgs/racket/share/pkgs/redex-lib/redex/private/judgment-form.rkt:330:0: call-judgment-form /home/racket/build-pkgs/racket/share/pkgs/redex-lib/redex/private/judgment-form.rkt:991:0: combine-judgment-rhses /home/racket/build-pkgs/racket/collects/racket/private/more-scheme.rkt:370:13: hash-ref! ... raco setup: making: /cur/lang raco setup: in /cur/lang raco setup: making: /cur/scribblings raco setup: making: /cur/scribblings/stdlib raco setup: making: /cur/stdlib raco setup: in /cur/stdlib raco setup: making: /cur/stdlib/tactics raco setup: in /cur/stdlib/tactics raco setup: --- creating launchers --- raco setup: --- installing man pages --- raco setup: --- building documentation --- raco setup: running: /cur/scribblings/cur.scrbl WARNING: collected information for key multiple times: '(dep ((lib "cur/main.rkt") Type)); values: #t #t WARNING: collected information for key multiple times: '(form ((lib "cur/main.rkt") Type)); values: (vector #f '(form ((lib "cur/main.rkt") Type)) #f (list (mobile-root #) #"Curnel_Forms.html") #f) (vector #f '(form ((lib "cur/main.rkt") Type)) #f (list (mobile-root #) #"Curnel_Forms.html") #f) WARNING: collected information for key multiple times: '(index-entry (form ((lib "cur/main.rkt") Type))); values: (list '("Type") (list (cached-element (style "RktSym" '(tt-chars #(struct:css-addition (collects #"scribble" #"racket.css")) #(struct:tex-addition (collects #"scribble" #"racket.tex")))) "Type" ...)) (delayed-index-desc #/racket-index/scribblings/main/user/local-redirect.scrbl raco setup: running: /racket-index/scribblings/main/user/release.scrbl raco setup: running: /racket-index/scribblings/main/user/search.scrbl raco setup: running: /racket-index/scribblings/main/user/start.scrbl raco setup: WARNING: undefined tag in /cur/scribblings/cur.scrbl: raco setup: (tech "goal") raco setup: (mod-path "cur/curnel/redex-lang") raco setup: (mod-path "cur/examples/stlc") raco setup: (tech "proof state") raco setup: rendering: /cur/scribblings/cur.scrbl WARNING: collected information for key multiple times: '(dep ((lib "cur/main.rkt") Type)); values: #t #t WARNING: collected information for key multiple times: '(form ((lib "cur/main.rkt") Type)); values: (vector #f '(form ((lib "cur/main.rkt") Type)) #f (list (mobile-root #) #"Curnel_Forms.html") #f) (vector #f '(form ((lib "cur/main.rkt") Type)) #f (list (mobile-root #) #"Curnel_Forms.html") #f) WARNING: collected information for key multiple times: '(index-entry (form ((lib "cur/main.rkt") Type))); values: (list '("Type") (list (cached-element (style "RktSym" (list 'tt-chars (css-addition '(collects #"scribble" #"racket.css")) (tex-addition '(collects #"scribble" #"racket.tex")))) "Type" ...)) (delayed-index-desc #)) (list '("Type") (list (cached-element (style "RktSym" (list 'tt-chars (css-addition '(collects #"scribble" #"racket.css")) (tex-addition '(collects #"scribble" #"racket.tex")))) "Type" ...)) (delayed-index-desc #)) raco setup: rendering: /racket-index/scribblings/main/user/local-redirect.scrbl raco setup: rendering: /racket-index/scribblings/main/user/release.scrbl raco setup: rendering: /racket-index/scribblings/main/user/search.scrbl raco setup: rendering: /racket-index/scribblings/main/user/start.scrbl raco setup: --- installing collections --- raco setup: --- post-installing collections --- raco setup: --- summary of errors --- raco setup: error: during making for /cur/examples raco setup: Church-Rosser broken (((((((((((((((((((((∅ (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Var : (Unv 0) ((avar : (Π (g5263 : Nat) Var))))) (Maybe : (Π (A : (Unv 0)) (Unv 0)) ((none : (Π (A : (Unv 0)) (Maybe A))) (some : (Π (A : (Unv 0)) (Π (a : A) (Maybe A))))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (True : (Unv 0) ((T : True)))) (False : (Unv 0) ())) (And : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : A) (Π (y : B) ((And A) B))))))))) (== : (Π (A : (Unv 0)) (Π (x : A) (Π (g6949 : A) (Unv 0)))) ((refl : (Π (A : (Unv 0)) (Π (x : A) (((== A) x) x))))))) (stlc-val : (Unv 0) ((stlc-true : stlc-val) (stlc-false : stlc-val) (stlc-unit : stlc-val)))) (stlc-type : (Unv 0) ((stlc-boolty : stlc-type) (stlc-unitty : stlc-type) (stlc--> : (Π (g7411 : stlc-type) (Π (g7412 : stlc-type) stlc-type))) (stlc-* : (Π (g7413 : stlc-type) (Π (g7414 : stlc-type) stlc-type)))))) (stlc-term : (Unv 0) ((Var-->-stlc-term : (Π (g7415 : Var) stlc-term)) (stlc-val-->-stlc-term : (Π (g7416 : stlc-val) stlc-term)) (stlc-app : (Π (g7417 : stlc-term) (Π (g7418 : stlc-term) stlc-term))) (stlc-lambda : (Π (g7419 : Var) (Π (g7420 : stlc-type) (Π (g7421 : stlc-term) stlc-term)))) (stlc-cons : (Π (g7422 : stlc-term) (Π (g7423 : stlc-term) stlc-term))) (stlc-let : (Π (g7424 : Var) (Π (g7425 : Var) (Π (g7426 : stlc-term) (Π (g7427 : stlc-term) stlc-term)))))))) (Gamma : (Unv 0) ((emp-gamma : Gamma) (extend-gamma : (Π (g7428 : Gamma) (Π (g7429 : Var) (Π (g7430 : stlc-type) Gamma))))))) (Π (g2 : (Maybe stlc-type)) (Unv 0))) ((((((((((((((((((((∅ (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Var : (Unv 0) ((avar : (Π (g5263 : Nat) Var))))) (Maybe : (Π (A : (Unv 0)) (Unv 0)) ((none : (Π (A : (Unv 0)) (Maybe A))) (some : (Π (A : (Unv 0)) (Π (a : A) (Maybe A))))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (True : (Unv 0) ((T : True)))) (False : (Unv 0) ())) (And : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : A) (Π (y : B) ((And A) B))))))))) (== : (Π (A : (Unv 0)) (Π (x : A) (Π (g6949 : A) (Unv 0)))) ((refl : (Π (A : (Unv 0)) (Π (x : A) (((== A) x) x))))))) (stlc-val : (Unv 0) ((stlc-true : stlc-val) (stlc-false : stlc-val) (stlc-unit : stlc-val)))) (stlc-type : (Unv 0) ((stlc-boolty : stlc-type) (stlc-unitty : stlc-type) (stlc--> : (Π (g7411 : stlc-type) (Π (g7412 : stlc-type) stlc-type))) (stlc-* : (Π (g7413 : stlc-type) (Π (g7414 : stlc-type) stlc-type)))))) (stlc-term : (Unv 0) ((Var-->-stlc-term : (Π (g7415 : Var) stlc-term)) (stlc-val-->-stlc-term : (Π (g7416 : stlc-val) stlc-term)) (stlc-app : (Π (g7417 : stlc-term) (Π (g7418 : stlc-term) stlc-term))) (stlc-lambda : (Π (g7419 : Var) (Π (g7420 : stlc-type) (Π (g7421 : stlc-term) stlc-term)))) (stlc-cons : (Π (g7422 : stlc-term) (Π (g7423 : stlc-term) stlc-term))) (stlc-let : (Π (g7424 : Var) (Π (g7425 : Var) (Π (g7426 : stlc-term) (Π (g7427 : stlc-term) stlc-term)))))))) (Gamma : (Unv 0) ((emp-gamma : Gamma) (extend-gamma : (Π (g7428 : Gamma) (Π (g7429 : Var) (Π (g7430 : stlc-type) Gamma))))))) (Π (g3 : (Maybe stlc-type)) (Unv 0))) ((((((((((((((((((((∅ (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (Nat : (Unv 0) ((z : Nat) (s : (Π (g4807 : Nat) Nat))))) (Var : (Unv 0) ((avar : (Π (g5263 : Nat) Var))))) (Maybe : (Π (A : (Unv 0)) (Unv 0)) ((none : (Π (A : (Unv 0)) (Maybe A))) (some : (Π (A : (Unv 0)) (Π (a : A) (Maybe A))))))) (Bool : (Unv 0) ((true : Bool) (false : Bool)))) (True : (Unv 0) ((T : True)))) (False : (Unv 0) ())) (And : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : A) (Π (y : B) ((And A) B))))))))) (== : (Π (A : (Unv 0)) (Π (x : A) (Π (g6949 : A) (Unv 0)))) ((refl : (Π (A : (Unv 0)) (Π (x : A) (((== A) x) x))))))) (stlc-val : (Unv 0) ((stlc-true : stlc-val) (stlc-false : stlc-val) (stlc-unit : stlc-val)))) (stlc-type : (Unv 0) ((stlc-boolty : stlc-type) (stlc-unitty : stlc-type) (stlc--> : (Π (g7411 : stlc-type) (Π (g7412 : stlc-type) stlc-type))) (stlc-* : (Π (g7413 : stlc-type) (Π (g7414 : stlc-type) stlc-type)))))) (stlc-term : (Unv 0) ((Var-->-stlc-term : (Π (g7415 : Var) stlc-term)) (stlc-val-->-stlc-term : (Π (g7416 : stlc-val) stlc-term)) (stlc-app : (Π (g7417 : stlc-term) (Π (g7418 : stlc-term) stlc-term))) (stlc-lambda : (Π (g7419 : Var) (Π (g7420 : stlc-type) (Π (g7421 : stlc-term) stlc-term)))) (stlc-cons : (Π (g7422 : stlc-term) (Π (g7423 : stlc-term) stlc-term))) (stlc-let : (Π (g7424 : Var) (Π (g7425 : Var) (Π (g7426 : stlc-term) (Π (g7427 : stlc-term) stlc-term)))))))) (Gamma : (Unv 0) ((emp-gamma : Gamma) (extend-gamma : (Π (g7428 : Gamma) (Π (g7429 : Var) (Π (g7430 : stlc-type) Gamma))))))) (Π (g4 : (Maybe stlc-type)) (Unv 0)))) raco setup: compiling: /cur/examples/stlc.rkt raco pkg install: packages installed, although setup reported errors The time is now Saturday, October 3rd, 2015 6:13:11am