From 43f35b2b4980ba1148fce6d5ca1db1b3062a49bb Mon Sep 17 00:00:00 2001
From: Jonathan Sterling <jonsterling@users.noreply.github.com>
Date: Tue, 21 Nov 2017 11:31:33 -0500
Subject: [PATCH] Proposal for improvements to concrete notation (#456)

* starting to cleanup tactic notation

* make the comma mean fewer things

* use "assert" rather than "let" for cut, unify bracketing

* use fresh...in rather than fresh...->

* try renaming 'assert' to 'claim'

* update Emacs mode a bit

* begin to put @favonia's Invincible Thought into practice

* get rid of more commas

* resolve #376

* allow underscores in fresh ->

* proof is easy now

* update failure tests

* Revert "proof is easy now"

This reverts commit 9d001d47cbf70f384fe08022ea22e945e180be83.

* resolve #468

* crappy fix for #469 (really need to rethink the grammar)

resolves #469

* update ua.prl
---
 emacs/redprl.el                               |  24 ++--
 script/mlyacclex.sh                           |   4 +
 src/redprl/redprl.grm                         |  60 ++++-----
 src/redprl/redprl.lex                         |   1 +
 test/examples.prl                             |  45 ++++---
 test/failure/lexical-error.prl                |   2 +-
 test/success/J.prl                            |   2 +-
 test/success/V-types.prl                      |  53 ++++----
 test/success/bool-fhcom-without-open-eval.prl |  14 +-
 test/success/connection.prl                   |  10 +-
 test/success/decomposition.prl                |  12 +-
 test/success/discrete-types.prl               |   2 +-
 test/success/equality-elim.prl                |  10 +-
 test/success/equality.prl                     |   4 +-
 test/success/hcom.prl                         |  16 +--
 test/success/hlevels.prl                      |  33 ++---
 test/success/lines.prl                        |   2 +-
 test/success/logical-investigations.prl       |  16 +--
 test/success/match.prl                        |   6 +-
 test/success/num.prl                          |  54 ++++----
 test/success/path-ap-const.prl                |   2 +-
 test/success/pi1s1.prl                        |  44 +++---
 test/success/primitive-sequencing.prl         |   2 +-
 test/success/pushout.prl                      |   4 +-
 test/success/record.prl                       |   8 +-
 test/success/semi-simplicial.prl              |  73 +++++-----
 test/success/strict-bool.prl                  |   2 +-
 test/success/theorem-of-choice.prl            |   6 +-
 test/success/unfold.prl                       |   6 +-
 test/success/wbool-fhcom.prl                  |   2 +-
 test/wip/ua.prl                               | 127 +++++++++---------
 31 files changed, 327 insertions(+), 319 deletions(-)
 create mode 100755 script/mlyacclex.sh

diff --git a/emacs/redprl.el b/emacs/redprl.el
index 91789a3ac..b045422b1 100644
--- a/emacs/redprl.el
+++ b/emacs/redprl.el
@@ -129,12 +129,12 @@
   "RedPRL's expression keywords.")
 
 (defconst redprl-expression-symbols
-  '("->" "~>" "<~" "$" "*" "!" "@" "=" "+" "++")
+  '("->" "~>" "<~" "$" "*" "!" "@" "=" "+" "++" "=>")
   "RedPRL's expression symbols.")
 
 (defconst redprl-tactic-keywords
   '("auto" "auto-step" "case" "cut-lemma" "elim" "else" "exact" "fresh" "goal"
-    "hyp" "id" "lemma" "let" "match" "of" "print" "progress"
+    "hyp" "id" "lemma" "let" "claim" "match" "of" "print" "progress"
     "query" "rec" "reduce" "refine" "repeat" "rewrite" "rewrite-hyp" "symmetry"
     "then" "unfold" "use" "with")
   "RedPRL's tactic keywords.")
@@ -160,18 +160,10 @@
 (defconst redprl-tac-name-regexp
   '(: "Tac" (+ whitespace) (group-n 1 (+ word)) not-wordchar))
 
-(defconst redprl-sym-name-regexp
-  '(: "Sym" (+ whitespace) (group-n 1 (+ word)) not-wordchar))
-
-(defconst redprl-record-name-regexp
-  '(: "Record" (+ whitespace) (group-n 1 (+ word)) not-wordchar))
-
 (defconst redprl-declaration-name-regexp
   `(or ,redprl-def-name-regexp
        ,redprl-thm-name-regexp
-       ,redprl-tac-name-regexp
-       ,redprl-sym-name-regexp
-       ,redprl-record-name-regexp))
+       ,redprl-tac-name-regexp))
 
 (defvar redprl-mode-font-lock-keywords
   `(
@@ -219,8 +211,10 @@
            (end-pos (match-end 0))
            (candidates (cl-remove-if-not
                         (apply-partially #'string-prefix-p match)
-                        (append redprl-keywords
-                                redprl-builtin-sorts
+                        (append redprl-tactic-keywords
+                                redprl-expression-keywords
+                                redprl-sequent-keywords
+                                redprl-sort-keywords
                                 (redprl-defined-names)))))
       (if (null candidates)
           nil
@@ -280,9 +274,7 @@
   (set (make-local-variable 'imenu-generic-expression)
        `(("Def" ,(rx-to-string redprl-def-name-regexp) 1)
          ("Thm" ,(rx-to-string redprl-thm-name-regexp) 1)
-         ("Tac" ,(rx-to-string redprl-tac-name-regexp) 1)
-         ("Sym" ,(rx-to-string redprl-sym-name-regexp) 1)
-         ("Record" ,(rx-to-string redprl-record-name-regexp) 1)))
+         ("Tac" ,(rx-to-string redprl-tac-name-regexp) 1)))
 
   ;; Bind mode-specific commands to keys
   (define-key redprl-mode-map (kbd "C-c C-l") 'redprl-compile-buffer)
diff --git a/script/mlyacclex.sh b/script/mlyacclex.sh
new file mode 100755
index 000000000..10e830dac
--- /dev/null
+++ b/script/mlyacclex.sh
@@ -0,0 +1,4 @@
+#!/bin/bash
+
+mlyacc src/redprl/redprl.grm
+mllex src/redprl/redprl.lex
diff --git a/src/redprl/redprl.grm b/src/redprl/redprl.grm
index dc28ceb8d..ebc362050 100644
--- a/src/redprl/redprl.grm
+++ b/src/redprl/redprl.grm
@@ -342,7 +342,7 @@ end
  (* keywords in tactics *)
  | CASE | OF
  | FRESH
- | LET | USE | WITH
+ | LET | CLAIM | USE | WITH
  | THEN | ELSE
  | REFINE
  | MTAC_REC | MTAC_PROGRESS | MTAC_REPEAT | MTAC_AUTO | MTAC_HOLE
@@ -468,9 +468,7 @@ end
  | devMatchClauses of (string list * (ast * ast)) list
  | selector of ast
  | selectors of ast list
- | bracketedSelectors of ast list
  | opnames of string list
- | bracketedOpnames of string list
 
  | declArgument of metavariable * Ar.valence
  | declArguments of string Signature.arguments
@@ -677,7 +675,7 @@ patvar
   | PERCENT VARNAME ((VARNAME, O.EXP))
 
 patvarBindings
-  : VARNAME COMMA patvarBindings (VARNAME :: patvarBindings)
+  : VARNAME patvarBindings (VARNAME :: patvarBindings)
   | VARNAME ([VARNAME])
 
 rawTermAndTac
@@ -741,6 +739,13 @@ rawTermAndTac
   | LPAREN ABS LSQUARE boundVars RSQUARE term RPAREN (Multi.makeAbs boundVars term)
   | LPAREN AT_SIGN term dimensions RPAREN (Multi.makeDimApp term dimensions)
 
+  (* levels *)
+  | LPAREN PLUS level NUMERAL RPAREN (Ast.$$ (O.LPLUS NUMERAL, [Ast.\ ([], level)]))
+  | LPAREN DOUBLE_PLUS level RPAREN (Ast.$$ (O.LPLUS 1, [Ast.\ ([], level)]))
+  | LPAREN LMAX levels RPAREN (Ast.$$ (O.LMAX, [\ ([], Multi.makeVec O.LVL levels)]))
+  | LOMEGA (Ast.$$ (O.LOMEGA, []))
+
+
 level
   : NUMERAL (Ast.$$ (O.LCONST NUMERAL, []))
   | LPAREN PLUS level NUMERAL RPAREN (Ast.$$ (O.LPLUS NUMERAL, [Ast.\ ([], level)]))
@@ -813,7 +818,7 @@ devDecompPattern
   | LBRACKET tupleDecompPattern RBRACKET (O.PAT_TUPLE tupleDecompPattern)
 
 devDecompPatterns
-  : devDecompPattern COMMA devDecompPatterns (devDecompPattern :: devDecompPatterns)
+  : devDecompPattern devDecompPatterns (devDecompPattern :: devDecompPatterns)
   | devDecompPattern ([devDecompPattern])
 
 labeledDecompPattern
@@ -845,25 +850,16 @@ selector
   | elimTargetAnySort (Ast.$$ (O.SEL_HYP, [Ast.\ ([], elimTargetAnySort)]))
 
 selectors
-  : selector COMMA selectors (selector :: selectors)
-  | selector ([selector])
-
-bracketedSelectors
-  : LSQUARE selectors RSQUARE (selectors)
+  : selector selectors (selector :: selectors)
   | selector ([selector])
 
 opnames
-  : OPNAME COMMA opnames (OPNAME :: opnames)
-  | OPNAME ([OPNAME])
-
-bracketedOpnames
-  : LSQUARE opnames RSQUARE (opnames)
+  : OPNAME opnames (OPNAME :: opnames)
   | OPNAME ([OPNAME])
 
 termAnySort
   : term (Ast.$$ (O.MK_ANY NONE, [Ast.\ ([], term)]))
 
-
 termsAnySort
   : termAnySort ([termAnySort])
   | termAnySort termsAnySort (termAnySort :: termsAnySort)
@@ -888,9 +884,9 @@ atomicRawTac
   | TAC_REWRITE_HYP elimTargetAnySort (Ast.$$ (O.TAC_REWRITE_HYP, [Ast.\ ([], Ast.$$ (O.SEL_CONCL, [])), Ast.\ ([], elimTargetAnySort)]))
   | TAC_REWRITE_HYP elimTargetAnySort IN selector (Ast.$$ (O.TAC_REWRITE_HYP, [Ast.\ ([], selector), Ast.\ ([], elimTargetAnySort)]))
   | TAC_REDUCE (Ast.$$ (O.TAC_REDUCE_ALL, []))
-  | TAC_REDUCE IN bracketedSelectors (Ast.$$ (O.TAC_REDUCE, [Ast.\ ([], Multi.makeVec O.SEL bracketedSelectors)]))
-  | TAC_UNFOLD bracketedOpnames (Ast.$$ (O.TAC_UNFOLD_ALL bracketedOpnames, []))
-  | TAC_UNFOLD bracketedOpnames IN bracketedSelectors (Ast.$$ (O.TAC_UNFOLD (bracketedOpnames), [Ast.\ ([], Multi.makeVec O.SEL bracketedSelectors)]))
+  | TAC_REDUCE IN selectors (Ast.$$ (O.TAC_REDUCE, [Ast.\ ([], Multi.makeVec O.SEL selectors)]))
+  | TAC_UNFOLD opnames (Ast.$$ (O.TAC_UNFOLD_ALL opnames, []))
+  | TAC_UNFOLD opnames IN selectors (Ast.$$ (O.TAC_UNFOLD (opnames), [Ast.\ ([], Multi.makeVec O.SEL selectors)]))
 
   | BACK_TICK termAnySort (Tac.exactAuto termAnySort)
   | RULE_EXACT termAnySort (Tac.exact termAnySort)
@@ -899,21 +895,21 @@ atomicRawTac
 
   | atomicTac DOUBLE_PIPE tactic %prec DOUBLE_PIPE (Tac.orElse (atomicTac, tactic))
 
-  | LAMBDA devDecompPatterns DOT tactic (Pattern.makeLambda devDecompPatterns tactic)
-  | LANGLE boundVars RANGLE tactic (Ast.$$ (O.DEV_PATH_INTRO (List.length boundVars), [\ (Multi.addUnderscores boundVars, tactic)]))
+  | LAMBDA devDecompPatterns DOUBLE_RIGHT_ARROW tactic (Pattern.makeLambda devDecompPatterns tactic)
+  | ABS boundVars DOUBLE_RIGHT_ARROW tactic (Ast.$$ (O.DEV_PATH_INTRO (List.length boundVars), [\ (Multi.addUnderscores boundVars, tactic)]))
   | LBRACKET recordFieldTactics RBRACKET (Multi.recordIntro (Pos.pos (LBRACKET1left fileName) (RBRACKET1right fileName)) recordFieldTactics)
   | LBRACKET tactics RBRACKET (Multi.sigmaIntro tactics)
   
   | IF elimTarget THEN tactic ELSE tactic
       (Ast.$$ (O.DEV_BOOL_ELIM, [\ ([], elimTarget), \ ([], tactic1), \ ([], tactic2)]))
 
-  | LET VARNAME COLON LSQUARE judgment RSQUARE EQUALS tactic DOT tactic
+  | CLAIM VARNAME COLON LSQUARE judgment RSQUARE BY LSQUARE tactic RSQUARE SEMI tactic
       (Ast.$$ (O.DEV_LET NONE, [\ ([], judgment), \ ([], tactic1), \([VARNAME], tactic2)]))
 
-  | LET devDecompPattern EQUALS elimTargetAnySort bracketedDevAppSpine DOT tactic
+  | LET devDecompPattern EQUALS elimTargetAnySort bracketedDevAppSpine SEMI tactic
       (Pattern.makeApplyHyp devDecompPattern elimTargetAnySort bracketedDevAppSpine tactic)
 
-  | LET devDecompPattern EQUALS customOpTerm bracketedDevAppSpine DOT tactic (Pattern.makeApplyLemma devDecompPattern customOpTerm bracketedDevAppSpine tactic)
+  | LET devDecompPattern EQUALS customOpTerm bracketedDevAppSpine SEMI tactic (Pattern.makeApplyLemma devDecompPattern customOpTerm bracketedDevAppSpine tactic)
 
   | USE elimTargetAnySort bracketedDevAppSpine (Pattern.makeUseHyp elimTargetAnySort bracketedDevAppSpine)
   | USE customOpTerm bracketedDevAppSpine (Pattern.makeUseLemma customOpTerm bracketedDevAppSpine)
@@ -922,7 +918,7 @@ atomicRawTac
       (Ast.$$ (O.DEV_S1_ELIM, [\ ([], elimTarget), \ ([], tactic1), \([VARNAME], tactic2)]))
 
   | MATCH termAnySort LBRACKET devMatchClauses RBRACKET (Tac.makeMatch termAnySort devMatchClauses)
-  | QUERY VARNAME LEFT_ARROW selector DOT tactic (Ast.$$ (O.DEV_QUERY, [\ ([], selector), \ ([VARNAME], tactic)]))
+  | QUERY VARNAME LEFT_ARROW selector SEMI tactic (Ast.$$ (O.DEV_QUERY, [\ ([], selector), \ ([VARNAME], tactic)]))
   | PRINT termAnySort (Ast.$$ (O.DEV_PRINT, [\ ([], termAnySort)]))
 
   (* overlapping with term *)
@@ -936,9 +932,10 @@ atomicRawMultitac
   | MTAC_REPEAT LBRACKET multitac RBRACKET (Ast.$$ (O.MTAC_REPEAT, [\ ([], multitac)]))
   | MTAC_AUTO (Tac.autoMtac)
   | MTAC_PROGRESS LBRACKET multitac RBRACKET (Ast.$$ (O.MTAC_PROGRESS, [\ ([], multitac)]))
-  | MTAC_REC VARNAME IN LBRACKET multitac RBRACKET (Ast.$$ (O.MTAC_REC, [\ ([VARNAME], multitac)]))
+  | MTAC_REC VARNAME DOUBLE_RIGHT_ARROW LBRACKET multitac RBRACKET (Ast.$$ (O.MTAC_REC, [\ ([VARNAME], multitac)]))
   | LPAREN multitac RPAREN (multitac)
-  | FRESH hypBindings RIGHT_ARROW atomicRawMultitac SEMI multitac %prec LEFT_ARROW (Tac.makeSeq atomicRawMultitac hypBindings multitac)
+  | FRESH hypBindings RIGHT_ARROW atomicRawMultitac %prec RIGHT_ARROW (Tac.makeSeq atomicRawMultitac hypBindings (Tac.tacToMultitac (Ast.$$ (O.TAC_ID, []))))
+  | FRESH hypBindings RIGHT_ARROW atomicRawMultitac SEMI multitac %prec RIGHT_ARROW (Tac.makeSeq atomicRawMultitac hypBindings multitac)
   | atomicTac %prec SEMI (Ast.$$ (O.MTAC_ALL, [\ ([], atomicTac)]))
   | QUESTION ident (Ast.$$ (O.MTAC_HOLE (SOME ident), []))
   | QUESTION (Ast.$$ (O.MTAC_HOLE NONE, []))
@@ -948,17 +945,17 @@ atomicMultitac
 
 rawMultitac
   : multitac SEMI atomicMultitac %prec SEMI (Tac.makeSeq multitac [] atomicMultitac)
+  | multitac SEMI (multitac)
   | atomicMultitac %prec SEMI (atomicMultitac)
 
 multitac : rawMultitac (annotate (Pos.pos (rawMultitac1left fileName) (rawMultitac1right fileName)) rawMultitac)
 
 hypBinding
-  : VARNAME COLON sort (VARNAME, sort)
-  | VARNAME (VARNAME, O.EXP)
+  : boundVar COLON sort (Option.getOpt (boundVar, "_"), sort)
+  | boundVar (Option.getOpt (boundVar, "_"), O.EXP)
 
 hypBindings
-  : hypBinding ([hypBinding])
-  | hypBinding COMMA hypBindings %prec COMMA (hypBinding :: hypBindings)
+  : hypBinding hypBindings %prec COMMA (hypBinding :: hypBindings)
   | ([])
 
 rawTactic
@@ -970,6 +967,7 @@ tactic
 tactics
   : tactic ([tactic])
   | tactic COMMA tactics (tactic :: tactics)
+  | tactic COMMA ([tactic])
 
 declArgument
   : metavar COLON valence ((metavar, valence))
diff --git a/src/redprl/redprl.lex b/src/redprl/redprl.lex
index 7d177e322..b06154a41 100644
--- a/src/redprl/redprl.lex
+++ b/src/redprl/redprl.lex
@@ -128,6 +128,7 @@ whitespace = [\ \t];
 "then"             => (Tokens.THEN (posTuple (size yytext)));
 "else"             => (Tokens.ELSE (posTuple (size yytext)));
 "let"              => (Tokens.LET (posTuple (size yytext)));
+"claim"            => (Tokens.CLAIM (posTuple (size yytext)));
 "use"              => (Tokens.USE (posTuple (size yytext)));
 "with"             => (Tokens.WITH (posTuple (size yytext)));
 "case"             => (Tokens.CASE (posTuple (size yytext)));
diff --git a/test/examples.prl b/test/examples.prl
index 2ac4cbd85..4ee631750 100644
--- a/test/examples.prl
+++ b/test/examples.prl
@@ -3,14 +3,14 @@ Thm BoolTest : [
 ] by [
   // A term/witness can be supplied to the refiner at any point in a tactic script
   // using the quotation operator `.
-  (lam x. if x then `tt else `ff); auto
+  (lam x => if x then `tt else `ff); auto
 ].
 
 
 Thm PathTest : [
   (path [_] S1 base base)
 ] by [
-  <x> `(loop x)
+  abs x => `(loop x)
 ].
 
 Thm LowLevel : [
@@ -19,7 +19,7 @@ Thm LowLevel : [
     wbool)
 ] by [
   fresh f -> refine fun/intro;
-  [fresh x, x/eq -> elim f;
+  [fresh x x/eq -> elim f;
   [`tt, use x],
   refine fun/eqtype;
   refine wbool/eqtype]
@@ -33,7 +33,7 @@ Thm LowLevel2 : [
     wbool)
 ] by [
   fresh f -> repeat {refine fun/intro; [id, auto]};
-  fresh x, x/eq -> elim f;
+  fresh x x/eq -> elim f;
   [`tt, use x]
 ].
 
@@ -44,11 +44,11 @@ Thm FunElimTest : [
    (-> wbool wbool)
    wbool)
 ] by [
-  lam f. use f [`tt]
+  lam f => use f [`tt]
 ].
 
 Thm S1ElimTest : [ (-> S1 S1) ] by [
-  lam s.
+  lam s =>
     case s of 
        base => `base
      | loop x => `(loop x)
@@ -82,7 +82,7 @@ Print BoolEta.
 Thm BoolEtaFunction : [
   (-> wbool wbool)
 ] by [
-  (lam b. if b then `tt else `ff); auto
+  (lam b => if b then `tt else `ff); auto
 ].
 
 Extract BoolEtaFunction.
@@ -103,14 +103,15 @@ Thm PathTest2 : [
     (lam [b] (BoolEta b)))
 ] by [
   // abstract a dimension
-  <x>
+  abs x =>
     // now, we are constructing a line of functions; so we use a
     // lambda.
-    (lam b.
+    (lam b =>
       // for our b:wbool, we will construct a path between b and
       // (BoolEta b).
-      let p : [(path [_] wbool b (BoolEta b))] =
-        if b then <y> `tt else <y> `ff.
+      claim p : [(path [_] wbool b (BoolEta b))] by [
+        if b then abs y => `tt else abs y => `ff
+      ];
 
       // Now, we will project the 'x'-side of our path. In the
       // interactive tactic environment, dimension expressions are
@@ -144,7 +145,7 @@ Thm PathTest3 : [
 Print PathTest3.
 
 Thm PairTest : [ (* [a : S1] (path [_] S1 a base)) ] by [
-  {`base, <x> `(loop x)}
+  {`base, abs x => `(loop x)}
 ].
 
 
@@ -164,7 +165,7 @@ Def Test = [
 Print Test.
 
 Thm SNot : [(-> bool bool)] by [
-  lam b. if b then `ff else `tt
+  lam b => if b then `ff else `tt
 ].
 
 Thm StrictBoolTest : [ SNot = (Cmp SNot (Cmp SNot SNot)) in (-> bool bool) ] by [
@@ -172,7 +173,7 @@ Thm StrictBoolTest : [ SNot = (Cmp SNot (Cmp SNot SNot)) in (-> bool bool) ] by
 ].
 
 Thm Not : [(-> [_ : wbool] wbool)] by [
-  (lam x. if x then `ff else `tt); auto
+  (lam x => if x then `ff else `tt); auto
 ].
 
 Thm FunExt(#l:lvl) : [
@@ -182,16 +183,16 @@ Thm FunExt(#l:lvl) : [
    [p : (-> [y : a] (path [_] b ($ f y) ($ g y)))]
    (path [_] (-> a b) f g))
 ] by [
-  lam a, b, f, g, p.
-    <i> lam x. use p [use x, `i]
+  lam a b f g p =>
+    abs i => lam x => use p [use x, `i]
 ].
 
 Print FunExt.
 
 Tac FunExtTac(#l : lvl) = [
-  query gl <- concl.
+  query gl <- concl;
   match gl {
-    [a, b, f, g, k| #jdg{(path [_] (-> %a %b) %f %g) true with %[k:knd]} =>
+    [a b f g k | #jdg{(path [_] (-> %a %b) %f %g) true with %[k:knd]} =>
       use (FunExt #l) [`%a, `%b, `%f, `%g, id]
     ]
   }
@@ -201,7 +202,7 @@ Print FunExtTac.
 
 Thm NotNotPath : [(path [_] (-> wbool wbool) (Cmp Not Not) (lam [x] x))] by [
   (FunExtTac #lvl{0});
-  (lam x. if x then <_> `tt else <_> `ff);
+  (lam x => if x then abs _ => `tt else abs _ => `ff);
   auto
 ].
 
@@ -210,11 +211,11 @@ Print FunExtTac.
 Print NotNotPath.
 
 Thm Singleton : [(* [x : wbool] (path [_] wbool x tt))] by [
-  {`tt, <_> `tt}
+  {`tt, abs _ => `tt}
 ].
 
 Thm PathElimTest : [(-> (path [_] bool tt tt) bool)] by [
-  lam x. use x [`(dim 0)]
+  lam x => use x [`(dim 0)]
 ].
 
 Thm PathEta(#l:lvl) : [
@@ -224,7 +225,7 @@ Thm PathEta(#l:lvl) : [
    (path [_] a m n)
    (path [_] a m n))
 ] by [
-  lam a, m, n, p. <j> use p [`j]
+  lam a m n p => abs j => use p [`j]
 ].
 
 Print PathEta.
diff --git a/test/failure/lexical-error.prl b/test/failure/lexical-error.prl
index e569d43ac..ebe7ce942 100644
--- a/test/failure/lexical-error.prl
+++ b/test/failure/lexical-error.prl
@@ -1,3 +1,3 @@
 Thm LexicalError : [ (-> bool bool) true ] by [
-  (lam x. `_tt); auto
+  (lam x => `_tt); auto
 ].
diff --git a/test/success/J.prl b/test/success/J.prl
index 54162e22a..eb10b6814 100644
--- a/test/success/J.prl
+++ b/test/success/J.prl
@@ -14,7 +14,7 @@ Thm J(#l:lvl) : [
    [p : (path [_] ty a x)]
    ($ fam x p))
 ] by [
-  lam ty, a, fam, d, x, p.
+  lam ty a fam d x p =>
     `(coe 0~>1
       [i] ($ fam
              (J/square i (dim 1) ty a p)
diff --git a/test/success/V-types.prl b/test/success/V-types.prl
index 552beb99b..f1f4c096e 100644
--- a/test/success/V-types.prl
+++ b/test/success/V-types.prl
@@ -13,15 +13,16 @@ Def Id = [(lam [a] a)].
 Thm IdIsEquiv(#l:lvl) : [
   (-> [ty : (U #l hcom)] (IsEquiv ty ty Id))
 ] by [
-  lam ty, a.
-  { {use a, <_> use a}
-  , lam {_,c'}. <i>
+  lam ty a =>
+  { {use a, abs _ => use a}
+  , lam {_,c'} => abs i =>
        { `(hcom 1~>0 ty a
            [i=0 [j] (@ c' j)]
            [i=1 [j] a])
-       , <j> `(hcom 1~>j ty a
-               [i=0 [j] (@ c' j)]
-               [i=1 [j] a])
+       , abs j =>
+          `(hcom 1~>j ty a
+            [i=0 [j] (@ c' j)]
+            [i=1 [j] a])
        }
   }
 ].
@@ -29,7 +30,7 @@ Thm IdIsEquiv(#l:lvl) : [
 Thm IdEquiv(#l:lvl) : [
   (-> [ty : (U #l hcom)] (Equiv ty ty))
 ] by [
-  lam ty.
+  lam ty =>
     {`Id, use (IdIsEquiv #l) [use ty]}
 ].
 
@@ -48,7 +49,7 @@ Thm IdV/Wf(#i:dim, #l:lvl) : [
    [ty : (U #l hcom)]
    (Member (IdV #i #l ty) (U #l)))
 ] by [
-  lam ty. `ax
+  lam ty => `ax
 ].
 
 Thm IdV/Test0(#i:dim, #l:lvl) : [
@@ -57,7 +58,7 @@ Thm IdV/Test0(#i:dim, #l:lvl) : [
    [a : ty]
    (Member (Vin #i a a) (IdV #i #l ty)))
 ] by [
-  lam ty, a. `ax
+  lam ty a => `ax
 ].
 
 Thm IdV/Test1(#l:lvl) : [
@@ -66,7 +67,7 @@ Thm IdV/Test1(#l:lvl) : [
    [a : ty]
    (= ty (Vproj (dim 0) (Vin (dim 0) a a) Id) a))
 ] by [
-  lam ty, a. auto
+  lam ty a => auto
 ].
 
 Thm IdV/Test2(#l:lvl) : [
@@ -76,7 +77,7 @@ Thm IdV/Test2(#l:lvl) : [
    (= ty (coe 0~>1 [x] (IdV x #l ty) a)
          (coe 0~>1 [_] ty a)))
 ] by [
-  lam ty, a. auto
+  lam ty a => auto
 ].
 
 Print IdV/Test2.
@@ -89,14 +90,15 @@ Thm Bool/reflect : [
   [p : (path [_] bool a b)]
   (= bool a b))
 ] by [
-  lam a, b, p. `(coe 0~>1 [x] (= bool a (@ p x)) ax)
+  lam a b p => `(coe 0~>1 [x] (= bool a (@ p x)) ax)
 ].
 
 Tac Bool/contra/inverse (#p:exp) = [
-  query gl <- concl.
+  query gl <- concl;
   match gl {
-    [a, b | #jdg{%a = %b in bool} =>
-      let eq : [(= bool %b %a)] = use Bool/reflect [`%b, `%a, `#p]; auto. symmetry; elim eq; auto
+    [a b | #jdg{%a = %b in bool} =>
+      claim eq : [(= bool %b %a)] by [use Bool/reflect [`%b, `%a, `#p]; auto];
+      symmetry; elim eq; auto
     ]
     [a | %[a:jdg] => id]
   }
@@ -105,16 +107,17 @@ Tac Bool/contra/inverse (#p:exp) = [
 Thm NotIsEquiv : [
   (IsEquiv bool bool Not)
 ] by [
-  lam b.
-  { {`($ Not b), <_> use b}
-  , lam {_,p'}.
-     (<i>
+  lam b =>
+  { {`($ Not b), abs _ => use b}
+  , lam {_,p'} =>
+     (abs i =>
         { `($ Not (hcom 1~>0 bool b
                     [i=0 [j] (@ p' j)]
                     [i=1 [j] b]))
-        , <j> `(hcom 1~>j bool b
-                [i=0 [j] (@ p' j)]
-                [i=1 [j] b])
+        , abs j =>
+            `(hcom 1~>j bool b
+              [i=0 [j] (@ p' j)]
+              [i=1 [j] b])
         }
       );
       auto; (Bool/contra/inverse p')
@@ -140,7 +143,7 @@ Thm NotV/Test0(#i:dim) : [
    [a : bool]
    (Member (Vin #i ($ Not a) a) (NotV #i)))
 ] by [
-  lam a. `ax
+  lam a => `ax
 ].
 
 Thm NotV/Test1 : [
@@ -148,7 +151,7 @@ Thm NotV/Test1 : [
    [a : bool]
    (= bool (coe 0~>1 [x] (NotV x) a) ($ Not a)))
 ] by [
-  lam a. auto
+  lam a => auto
 ].
 
 Thm NotV/Test2 : [
@@ -156,5 +159,5 @@ Thm NotV/Test2 : [
    [a : bool]
    (= bool (coe 1~>0 [x] (NotV x) a) ($ Not a)))
 ] by [
-  lam a. auto
+  lam a => auto
 ].
diff --git a/test/success/bool-fhcom-without-open-eval.prl b/test/success/bool-fhcom-without-open-eval.prl
index b3c6d7d3a..2ffb35322 100644
--- a/test/success/bool-fhcom-without-open-eval.prl
+++ b/test/success/bool-fhcom-without-open-eval.prl
@@ -5,8 +5,8 @@ Thm Fcom/trans3 : [
    (path [_] wbool b d)
    (path [_] wbool c d))
 ] by [
-  lam a, b, c, d, pab, pac, pbd.
-    <i> `(fcom 0~>1 (@ pab i) [i=0 [j] (@ pac j)] [i=1 [j] (@ pbd j)])
+  lam a b c d pab pac pbd =>
+    abs i => `(fcom 0~>1 (@ pab i) [i=0 [j] (@ pac j)] [i=1 [j] (@ pbd j)])
 ].
 
 Print Fcom/trans3.
@@ -17,8 +17,8 @@ Thm Fcom/trans2 : [
    (path [_] wbool b c)
    (path [_] wbool a c))
 ] by [
-  lam a, b, c, pab, pbc.
-    <i> `(fcom 0~>1 (@ pab i) [i=0 [_] a] [i=1 [j] (@ pbc j)])
+  lam a b c pab pbc =>
+    abs i => `(fcom 0~>1 (@ pab i) [i=0 [_] a] [i=1 [j] (@ pbc j)])
 ].
 
 Thm Fcom/symm : [
@@ -26,8 +26,8 @@ Thm Fcom/symm : [
    (path [_] wbool a b)
    (path [_] wbool b a))
 ] by [
-  lam a, b, pab.
-    <i> `(fcom 0~>1 a [i=0 [j] (@ pab j)] [i=1 [_] a])
+  lam a b pab =>
+    abs i => `(fcom 0~>1 a [i=0 [j] (@ pab j)] [i=1 [_] a])
 ].
 
 Thm Tube : [
@@ -35,7 +35,7 @@ Thm Tube : [
    [x : wbool]
    (= wbool (fcom 0~>1 x [1=1 [_] x] [0=0 [_] x]) x))
 ] by [
-  lam x. auto
+  lam x => auto
 ].
 
 Thm TrueByEvaluation : [
diff --git a/test/success/connection.prl b/test/success/connection.prl
index 2fc359355..d756f9717 100644
--- a/test/success/connection.prl
+++ b/test/success/connection.prl
@@ -5,8 +5,8 @@ Thm Connection(#l:lvl) : [
    [p : (path [_] ty a b)]
    (path [i] (path [_] ty a (@ p i)) (abs [_] a) p))
 ] by [
-  lam ty, a, b, p.
-    <i j>
+  lam ty a b p =>
+    abs i j =>
       `(hcom 0~>1 ty a
         [i=0 [k]
           (hcom 1~>j ty
@@ -42,8 +42,8 @@ Thm BetterConnection(#l:lvl) : [
    [p : (path [_] ty a b)]
    (path [i] (path [_] ty a (@ p i)) (abs [_] a) p))
 ] by [
-  lam ty, a, b, p.
-    <i j>
+  lam ty a b p =>
+    abs i j =>
       `(hcom 0~>1 ty a
         [i=0 [k]
          (hcom 1~>0 ty (@ p k)
@@ -74,7 +74,7 @@ Thm BetterConnectionTest0 (#l:lvl) : [
    [p : (path [_] ty a b)]
    (= (path [_] ty a b) (abs [i] (@ ($ (BetterConnection #l) ty a b p) i i)) p))
 ] by [
-  lam ty, a, b, p. unfold BetterConnection; auto
+  lam ty a b p => unfold BetterConnection; auto
 ].
 
 
diff --git a/test/success/decomposition.prl b/test/success/decomposition.prl
index b48e9f1b3..3a925ea3b 100644
--- a/test/success/decomposition.prl
+++ b/test/success/decomposition.prl
@@ -3,7 +3,7 @@ Thm Decomposition : [
    (record [foo : (record [a : bool] [b : (* bool bool)])] [bar : S1])
    bool)
 ] by [
-  lam {foo = {a = a, b = {welp}}}.
+  lam {foo = {a = a, b = {welp}}} =>
   use welp
 ].
 
@@ -20,8 +20,8 @@ Thm Apply : [
      (tuple [a base])))
    S1)
 ] by [
-  lam f.
-    let {a = a} = f [`tt, `ff, `(dim 0)].
+  lam f =>
+    let {a = a} = f [`tt, `ff, `(dim 0)];
     use a
 ].
 
@@ -30,8 +30,8 @@ Extract Apply.
 Thm UseHypTest : [
   (-> bool bool)
 ] by [
-  lam x.
-  let p : [(-> bool S1 bool)] = lam b, c. use b.
+  lam x =>
+  claim p : [(-> bool S1 bool)] by [lam b c => use b];
   use p [use x, `(loop 0)]
 ].
 
@@ -40,6 +40,6 @@ Print UseHypTest.
 Thm UseLemmaTest : [
   (-> bool bool)
 ] by [
-  lam x.
+  lam x =>
   use UseHypTest [use x]
 ].
\ No newline at end of file
diff --git a/test/success/discrete-types.prl b/test/success/discrete-types.prl
index 09247f599..825fcabb8 100644
--- a/test/success/discrete-types.prl
+++ b/test/success/discrete-types.prl
@@ -5,5 +5,5 @@ Thm Discrete/reflection(#l:lvl) : [
    [p : (path [_] ty a b)]
    (= ty a b))
 ] by [
-  lam ty, a, b, p. `(coe 0~>1 [x] (= ty a (@ p x)) ax)
+  lam ty a b p => `(coe 0~>1 [x] (= ty a (@ p x)) ax)
 ].
diff --git a/test/success/equality-elim.prl b/test/success/equality-elim.prl
index b4d1a9806..64d1fe6ba 100644
--- a/test/success/equality-elim.prl
+++ b/test/success/equality-elim.prl
@@ -1,16 +1,16 @@
 Tac GetHole(#c : [exp].exp, #t : [exp].tac) = [
-  query gl <- concl.
+  query gl <- concl;
   match gl {
     [hole | #jdg{(#c %hole)} => (#t %hole)]
   }
 ].
 
-// We can write a cool user-defined tactic for asserting and then rewriting along an equality.
+// We can write a cool user-defined tactic for claiming and then rewriting along an equality.
 // (Rewrite n a [x] c) matches the goal against the motive "[x] c" and rewrites along
 // the equality [_ = n in a].
 Tac Rewrite(#c : [exp].exp, #n, #a, #t : tac) = [
   (GetHole [x] (#c x) [hole] #tac{
-    let p : [hole = #n in #a] = #t.
+    claim p : [hole = #n in #a] by [#t];
     // Use the elimination rule for equality. We bind a new hypothesis which will represent the location
     // in the goal #c which is being rewritten.
     fresh x -> rewrite-hyp p;
@@ -22,11 +22,11 @@ Thm EqualityElimTest : [
   (-> [b : bool] (path [_] bool tt (if tt tt ff)))
 ] by [
   // We're going to prove this in a silly way to illustrate equality elimination.
-  // We'll rewrite the goal by asserting [(if tt tt ff) = tt in bool].
+  // We'll rewrite the goal by claiming [(if tt tt ff) = tt in bool].
   (Rewrite 
     [x] (-> bool (path [_] bool tt x))
     tt bool #tac{auto});
   // observe that the goal has now been rewritten!
   ?check-this-out;
-  lam b. <_> `tt
+  lam b => abs _ => `tt
 ].
diff --git a/test/success/equality.prl b/test/success/equality.prl
index 786f371eb..9d83a2cff 100644
--- a/test/success/equality.prl
+++ b/test/success/equality.prl
@@ -4,7 +4,7 @@ Thm EqualityKind0(#A) : [
    [a b : ty]
    (= (U 0 hcom) (= ty a b) (= ty a b)))
 ] by [ 
-  lam ty, a, b. auto
+  lam ty a b => auto
 ].
 
 Thm EqualityKind1(#A) : [
@@ -13,5 +13,5 @@ Thm EqualityKind1(#A) : [
    [a b : ty]
    (= (U 0 kan) (= ty a b) (= ty a b)))
 ] by [ 
-  lam ty, a, b. auto
+  lam ty a b => auto
 ].
\ No newline at end of file
diff --git a/test/success/hcom.prl b/test/success/hcom.prl
index 975b22bd4..9df45ba7e 100644
--- a/test/success/hcom.prl
+++ b/test/success/hcom.prl
@@ -7,8 +7,8 @@ Thm Hcom/Poly(#l:lvl) : [
    (path [_] ty b d)
    (path [_] ty c d))
 ] by [
-  lam ty, a, b, c, d, pab, pac, pbd.
-    <i>
+  lam ty a b c d pab pac pbd =>
+    abs i =>
       `(hcom 0~>1 ty (@ pab i)
         [i=0 [j] (@ pac j)]
         [i=1 [j] (@ pbd j)])
@@ -24,8 +24,8 @@ Thm Hcom/trans(#l:lvl) : [
    (path [_] ty b c)
    (path [_] ty a c))
 ] by [
-  lam ty, a, b, c, pab, pbc.
-    <i>
+  lam ty a b c pab pbc =>
+    abs i =>
       `(hcom 0 ~> 1 ty (@ pab i)
         [i=0 [_] a]
         [i=1 [j] (@ pbc j)])
@@ -40,8 +40,8 @@ Thm Hcom/symm(#l:lvl) : [
    (path [_] ty a b)
    (path [_] ty b a))
 ] by [
-  lam ty, a, b, pab.
-    <i>
+  lam ty a b pab =>
+    abs i =>
       `(hcom 0~>1 ty a
         [i=0 [j] (@ pab j)]
         [i=1 [_] a])
@@ -58,7 +58,7 @@ Thm Cap(#i:dim, #l:lvl) : [
       (hcom 0~>0 ty x [#i=0 [_] x] [#i=1 [_] x])
       x))
 ] by [
-  lam ty, x. auto
+  lam ty x => auto
 ].
 
 
@@ -71,7 +71,7 @@ Thm Tube(#l:lvl) : [
       (hcom 0~>1 ty x [1=1 [_] x] [0=0 [_] x])
       x))
 ] by [
-  lam ty, x. auto
+  lam ty x => auto
 ].
 
 Thm TrueByEvaluation : [
diff --git a/test/success/hlevels.prl b/test/success/hlevels.prl
index b8d09c035..293dac019 100644
--- a/test/success/hlevels.prl
+++ b/test/success/hlevels.prl
@@ -10,7 +10,7 @@ Thm InhPropIsContr(#l:lvl) : [
   [a : ty]
   (IsContr ty))
 ] by [
-  lam ty, h, a. {use a,lam x. `($ h x a)}
+  lam ty h a => {use a, lam x => `($ h x a)}
 ].
 
 Thm PropPi(#l:lvl) : [
@@ -20,22 +20,22 @@ Thm PropPi(#l:lvl) : [
   [h : (-> [x : tyA] (IsProp ($ tyB x)))]
   (IsProp (-> [x : tyA] ($ tyB x))))
 ] by [
-  lam tyA, tyB, h, f, g. <i> lam x. `(@ ($ h x ($ f x) ($ g x)) i)
+  lam tyA tyB h f g => abs i => lam x => `(@ ($ h x ($ f x) ($ g x)) i)
 ].
 
 Thm PropSet(#l:lvl) : [
   (->
    [tyA : (U #l kan)]
    [h : (IsProp tyA)]
-   (IsSet tyA)
-  )
+   (IsSet tyA))
 ] by [
-  lam tyA, h, a, b, p, q.
-  <j i> `(hcom 0~>1 tyA a
-               [i=0 [k] (@ ($ h a a) k)]
-               [i=1 [k] (@ ($ h a b) k)]
-               [j=0 [k] (@ ($ h a (@ p i)) k)]
-               [j=1 [k] (@ ($ h a (@ q i)) k)])
+  lam tyA h a b p q => 
+  abs j i =>
+    `(hcom 0~>1 tyA a
+      [i=0 [k] (@ ($ h a a) k)]
+      [i=1 [k] (@ ($ h a b) k)]
+      [j=0 [k] (@ ($ h a (@ p i)) k)]
+      [j=1 [k] (@ ($ h a (@ q i)) k)])
 ].
 
 // This proof should be easy, but it is not...
@@ -45,11 +45,12 @@ Thm IsPropIsProp(#l:lvl) : [
    (IsProp (IsProp tyA))
   )
 ] by [
-  lam tyA, h1, h2. // why is 1 and 2 blue?
-  <i> lam a, b.
-    let foo = (PropSet #l) [`tyA, `h1].
-    unfold [IsSet, IsProp];
-    use foo [`a, `b, use h1 [`a, `b], use h2 [`a, `b], `i]
+  lam tyA h1 h2 =>
+  (abs i => lam a b =>
+    let foo = (PropSet #l) [`tyA, `h1];
+    unfold IsSet IsProp;
+    use foo [`a, `b, use h1 [`a, `b], use h2 [`a, `b], `i]);
+  unfold PropSet; auto
 ].
 
 Thm IsPropIsProp'(#l:lvl) : [
@@ -58,7 +59,7 @@ Thm IsPropIsProp'(#l:lvl) : [
    (IsProp (IsProp tyA))
   )
 ] by [
-  lam tyA, h1, h2. <i> lam a, b. `(@ ($ (PropSet #l) tyA h1 a b ($ h1 a b) ($ h2 a b)) i)
+  lam tyA h1 h2 => abs i => lam a b => `(@ ($ (PropSet #l) tyA h1 a b ($ h1 a b) ($ h2 a b)) i)
 ].
 
 // // This should be exactly like the one above:
diff --git a/test/success/lines.prl b/test/success/lines.prl
index 04b3f459b..34775c52c 100644
--- a/test/success/lines.prl
+++ b/test/success/lines.prl
@@ -4,5 +4,5 @@ Thm Line/Test0 : [
    [l : (-> dim a)]
    (= a (coe 0~>1 [_] a (@ l 0)) (@ (coe 0~>1 [_] (-> dim a) l) 0)))
 ] by [
-  lam a, l. `ax
+  lam a l => `ax
 ].
diff --git a/test/success/logical-investigations.prl b/test/success/logical-investigations.prl
index bc59f1d6b..95c887890 100644
--- a/test/success/logical-investigations.prl
+++ b/test/success/logical-investigations.prl
@@ -5,7 +5,7 @@ Thm Thm1 : [
    [p q : (U 0)]
    p q p)
 ] by [
-  lam p, q, a, b. use a
+  lam p q a b => use a
 ].
 
 Thm Thm2 : [
@@ -15,7 +15,7 @@ Thm Thm2 : [
    (-> p q r)
    p r)
 ] by [
-  lam p, q, r, f, g, a.
+  lam p q r f g a =>
   use g [use a, use f [use a]]
 ].
 
@@ -30,7 +30,7 @@ Thm Thm3/low-level : [
    (-> q r)
    (-> p r))
 ] by [
-  fresh p, q, r, pq, qr, x -> repeat {refine fun/intro || id};
+  fresh p q r pq qr x -> repeat {refine fun/intro || id};
   auto;
   fresh z -> elim qr;
   [fresh y -> elim pq; [use x, use y], use z]
@@ -48,7 +48,7 @@ Thm Thm3/high-level : [
    (-> q r)
    (-> p r))
 ] by [
-  lam p, q, r, f, g, x.
+  lam p q r f g x =>
   use g [use f [use x]]
 ].
 
@@ -59,16 +59,16 @@ Def Not(#A) = [ (-> #A void) ].
 Thm Thm4 : [
   (-> [p q : (U 0)] (Not p) p q)
 ] by [
-  lam p, q, r, a.
+  lam p q r a =>
   unfold Not;
-  let boom = r [use a].
+  let boom = r [use a];
   elim boom
 ].
 
 Thm Thm5 : [
   (-> [p : (U 0)] p (Not (Not p)))
 ] by [
-  lam p, a. unfold Not; lam r.
+  lam p a => unfold Not; lam r =>
   use r [use a]
 ].
 
@@ -79,7 +79,7 @@ Print Thm5.
 Thm Thm6(#A,#B) : [
   (-> [p q : (U 0)] (-> p q) (Not q) (Not p))
 ] by [
-  lam p, q, f, g. unfold Not; lam a.
+  lam p q f g => unfold Not; lam a =>
   use g [use f [use a]]
 ].
 
diff --git a/test/success/match.prl b/test/success/match.prl
index 94a02ac9d..8dde3345d 100644
--- a/test/success/match.prl
+++ b/test/success/match.prl
@@ -1,15 +1,15 @@
 Tac QueryGoalType(#t : [exp].tac) = [
-  query gl <- concl.
+  query gl <- concl;
   match gl {
     [a | #jdg{%a true} => (#t %a)]
   }
 ].
 
 Thm MatchGoal : [ (-> bool bool bool bool bool bool) ] by [
-  fresh x, y -> repeat {
+  fresh x y -> repeat {
     (QueryGoalType [ty] #tac{
       match ty {
-        [a, b | (-> [x:%a] (%b x)) => refine fun/intro; [id, auto]]
+        [a b | (-> [x:%a] (%b x)) => refine fun/intro; [id, auto]]
       }
     })
   };
diff --git a/test/success/num.prl b/test/success/num.prl
index 633a6de9e..2fca8267d 100644
--- a/test/success/num.prl
+++ b/test/success/num.prl
@@ -19,23 +19,23 @@ Thm NatOne : [
 Thm NatIsInt : [
   (-> [x : nat] (= int x x))
 ] by [
-  lam x. fresh x', x'/ih -> elim x; auto
+  lam x => fresh x' x'/ih -> elim x; auto
 ].
 
 Thm Pred : [
   (-> nat nat)
 ] by [
-  lam a.
-  fresh a', ind -> elim a;
+  lam a =>
+  fresh a' ind -> elim a;
   [ `zero ];
   [ `a' ]
 ].
 
 // A tactic to infer and supply a simple (non-dependent) motive to the nat/eq/nat-rec rule.
 Tac SimpleNatRecEq = [
-  query gl <- concl.
+  query gl <- concl;
   match gl {
-    [n,z,s,ty | #jdg{(nat-rec %n %z [x y] (%s x y)) in %ty} =>
+    [n z s ty | #jdg{(nat-rec %n %z [x y] (%s x y)) in %ty} =>
       refine nat/eq/nat-rec; [`%ty]; auto]
   }
 ].
@@ -45,10 +45,10 @@ Print SimpleNatRecEq.
 Thm Plus : [
   (-> nat nat nat)
 ] by [
-  lam a.
-  fresh a', ind -> elim a;
-  [ lam x. use x
-  , lam x. let ih/x = ind [use x]. `(succ ih/x)
+  lam a =>
+  fresh a' ind -> elim a;
+  [ lam x => use x
+  , lam x => let ih/x = ind [use x]; `(succ ih/x)
   ]
 ].
 
@@ -61,14 +61,14 @@ Thm Plus/wf : [
 Thm Plus/zeroL : [
   (-> [n : nat] (= nat ($ Plus 0 n) n))
 ] by [
-  lam n. auto
+  lam n => auto
 ].
 
 Thm Plus/zero/R : [
   (-> [n : nat] (= nat ($ Plus n 0) n))
 ] by [
-  lam n.
-    fresh n', ind -> elim n;
+  lam n =>
+    fresh n' ind -> elim n;
     [ `ax
     , fresh x -> rewrite-hyp ind;
       [ `(= nat (succ x) (succ n'))
@@ -82,14 +82,14 @@ Thm Plus/zero/R : [
 Thm Plus/succ/L : [
   (-> [n m : nat] (= nat ($ Plus (succ n) m) (succ ($ Plus n m))))
 ] by [
-  lam n, m. auto; refine fun/eq/app; [`(-> nat nat)]; auto; SimpleNatRecEq
+  lam n m => auto; refine fun/eq/app; [`(-> nat nat)]; auto; SimpleNatRecEq
 ].
 
 
 Thm Plus/succ/R : [
   (-> [n m : nat] (= nat ($ Plus n (succ m)) (succ ($ Plus n m))))
 ] by [
-  lam n, m. fresh n', n'/ih -> elim n;
+  lam n m => fresh n' n'/ih -> elim n;
     [ auto
     , fresh x -> rewrite ($ Plus/succ/L n' (succ m));
       [ `(= nat x (succ ($ Plus (succ n') m)))
@@ -109,7 +109,7 @@ Thm Plus/succ/R : [
 Thm Plus/test0 : [
   (-> [n m : nat] [eq : (= nat ($ Plus n zero) m)] (= nat n m))
 ] by [
-  lam n, m, eq.
+  lam n m eq =>
     fresh x -> rewrite ($ Plus/zero/R n) in eq;
     [ `(= nat x m) ]; auto
 ].
@@ -117,13 +117,13 @@ Thm Plus/test0 : [
 Thm Eq/sym : [
   (-> [ty : (U 0)] [a b : ty] (= ty a b) (= ty b a))
 ] by [
-  lam ty, a, b, eq. symmetry; auto
+  lam ty a b eq => symmetry; auto
 ].
 
 Thm Plus/comm : [
   (-> [n m : nat] (= nat ($ Plus n m) ($ Plus m n)))
 ] by [
-  lam n, m. fresh n', n'/ih -> elim n;
+  lam n m => fresh n' n'/ih -> elim n;
     [ symmetry; `($ Plus/zero/R  m)
     , fresh x -> rewrite ($ Plus/succ/L n' m);
       [ `(= nat x ($ Plus m (succ n')))
@@ -143,8 +143,8 @@ Thm NatSymm : [
    (path [_] nat a b)
    (path [_] nat b a))
 ] by [
-  lam a, b, pab.
-  <i>
+  lam a b pab => 
+  abs i =>
     `(hcom 0~>1 nat a 
       [i=0 [j] (@ pab j)]
       [i=1 [_] a])
@@ -155,8 +155,8 @@ Print NatSymm.
 Thm IntPred : [
   (-> int int)
 ] by [
-  lam a. fresh a', junk -> elim a;
-  [ `-1, fresh n, junk -> elim a'; [`0, `(succ n)]
+  lam a => fresh a' _ -> elim a;
+  [ `-1, fresh n _ -> elim a'; [`0, `(succ n)]
   , `-2, `(negsucc (succ (succ a')))
   ]
 ].
@@ -164,7 +164,7 @@ Thm IntPred : [
 Thm IntSucc : [
   (-> int int)
 ] by [
-  lam a. fresh a', junk -> elim a;
+  lam a => fresh a' _ -> elim a;
   [ `1, `(succ (succ a'))
   , `0, `(negsucc a')
   ]
@@ -173,11 +173,11 @@ Thm IntSucc : [
 Thm IntPlus : [
   (-> int int int)
 ] by [
-  lam a. fresh a', ind -> elim a;
-  [ lam b. use b
-  , lam b. `($ IntSucc ($ ind b))
-  , lam b. `($ IntPred b)
-  , lam b. `($ IntPred ($ ind b))
+  lam a => fresh a' ind -> elim a;
+  [ lam b => use b
+  , lam b => `($ IntSucc ($ ind b))
+  , lam b => `($ IntPred b)
+  , lam b => `($ IntPred ($ ind b))
   ]
 ].
 
diff --git a/test/success/path-ap-const.prl b/test/success/path-ap-const.prl
index 92ec73dc8..101d5233d 100644
--- a/test/success/path-ap-const.prl
+++ b/test/success/path-ap-const.prl
@@ -1,7 +1,7 @@
 Thm PathApConst : [
   (-> (path [_] bool tt tt) bool)
 ] by [
-  lam p. use p [`(dim 0)]
+  lam p => use p [`(dim 0)]
 ].
 
 Print PathApConst.
diff --git a/test/success/pi1s1.prl b/test/success/pi1s1.prl
index ebc0fa83c..7e3d03672 100644
--- a/test/success/pi1s1.prl
+++ b/test/success/pi1s1.prl
@@ -1,14 +1,14 @@
 Thm IntSucc : [
   (-> int int)
 ] by [
-  lam i. `(int-rec i 1 [n _] (succ (succ n)) 0 [n _] (negsucc n));
+  lam i => `(int-rec i 1 [n _] (succ (succ n)) 0 [n _] (negsucc n));
     refine int/eq/int-rec; [ `int ]; auto
 ].
 
 Thm IntPred : [
   (-> int int)
 ] by [
-  lam i. `(int-rec i -1 [n _] (nat-rec n 0 [n _] (succ n)) -2 [n _] (negsucc (succ (succ n))));
+  lam i => `(int-rec i -1 [n _] (nat-rec n 0 [n _] (succ n)) -2 [n _] (negsucc (succ (succ n))));
     refine int/eq/int-rec; [ `int ]; auto;
     refine nat/eq/nat-rec; [ `int ]; auto
 ].
@@ -16,7 +16,7 @@ Thm IntPred : [
 Thm IntSuccIntPred : [
   (-> [i : int] (= int ($ IntSucc ($ IntPred i)) i))
 ] by [
-  lam i. fresh n -> elim i;
+  lam i => fresh n -> elim i;
     [ auto
     , elim n; auto
     , auto
@@ -27,7 +27,7 @@ Thm IntSuccIntPred : [
 Thm IntPredIntSucc : [
   (-> [i : int] (= int ($ IntPred ($ IntSucc i)) i))
 ] by [
-  lam i. fresh n -> elim i;
+  lam i => fresh n -> elim i;
     [ auto
     , auto
     , auto
@@ -48,20 +48,22 @@ Def Equiv (#A,#B) = [(* [f : (-> #A #B)] (IsEquiv #A #B f))].
 Thm IntSuccIsEquiv : [
   (IsEquiv int int IntSucc)
 ] by [
-  lam i.
-    let eq : [(= int ($ IntSucc ($ IntPred i)) i)] = `($ IntSuccIntPred i).
-      fresh eq' -> elim eq; unfold [IntSucc, IntPred] in eq'; reduce in eq';
+  lam i =>
+    claim eq : [(= int ($ IntSucc ($ IntPred i)) i)] by [use IntSuccIntPred [`i]];
+    fresh eq' -> elim eq; unfold IntSucc IntPred in eq'; reduce in eq';
     {
-      {`($ IntPred i), <_> `i}
-    , lam {i',p'}.
-        let eq0 : [(= int i ($ IntSucc i'))] = `(coe 1~>0 [x] (= int i (@ p' x)) ax).
-        let eq1 : [(= int ($ IntPred i) i')] = fresh i'' ->
-          rewrite eq0;
-          [`(= int ($ IntPred i'') i'), `($ IntPredIntSucc i')];
-          auto.
-
-        (<x>
-          {`($ IntPred i), <y> `(hcom 1~>y int i [x=0 [y] (@ p' y)] [x=1 [_] i])});
+      {use IntPred [`i], abs _ => `i}
+    , lam {i',p'} =>
+        claim eq0 : [(= int i ($ IntSucc i'))] by [`(coe 1~>0 [x] (= int i (@ p' x)) ax)];
+        claim eq1 : [(= int ($ IntPred i) i')] by [
+          fresh i'' ->
+            rewrite eq0;
+            [`(= int ($ IntPred i'') i'), `($ IntPredIntSucc i')];
+            auto
+        ];
+
+        (abs x =>
+          {`($ IntPred i), abs y => `(hcom 1~>y int i [x=0 [y] (@ p' y)] [x=1 [_] i])});
         
         auto; fresh eq1' -> elim eq1; unfold IntPred in eq1'; reduce in eq1'; auto
     }
@@ -76,13 +78,13 @@ Thm IntSuccEquiv : [
 Thm IntSuccPath : [
   (path [_] (U 0 kan) int int)
 ] by [
-  <x> `(V x int int IntSuccEquiv)
+  abs x => `(V x int int IntSuccEquiv)
 ].
 
 Thm S1UnivCover : [
   (-> S1 (U 0 kan))
 ] by [
-  lam x. exact (S1-rec [_] (U 0 kan) x int [x] (@ IntSuccPath x)); refine s1/eq/s1-rec; auto
+  lam x => exact (S1-rec [_] (U 0 kan) x int [x] (@ IntSuccPath x)); refine s1/eq/s1-rec; auto
 ].
 
 // Needs rewriting on types
@@ -108,8 +110,8 @@ Thm S1Concat : [
    [q : (path [_] S1 b c)]
    (path [_] S1 a c))
 ] by [
-  lam a, b, c, p, q.
-    <x> `(hcom 0~>1 S1 (@ p x) [x=0 [_] a] [x=1 [y] (@ q y)])
+  lam a b c p q =>
+    abs x => `(hcom 0~>1 S1 (@ p x) [x=0 [_] a] [x=1 [y] (@ q y)])
 ].
 
 Thm S1UnivCover/Test1 : [
diff --git a/test/success/primitive-sequencing.prl b/test/success/primitive-sequencing.prl
index 538759cca..bd3ea55d5 100644
--- a/test/success/primitive-sequencing.prl
+++ b/test/success/primitive-sequencing.prl
@@ -1,5 +1,5 @@
 Thm PrimitiveSequencingTest : [(-> bool bool bool bool)] by [
-  fresh x,y,z -> repeat {refine fun/intro || id}; auto;
+  fresh x y z -> repeat {refine fun/intro || id}; auto;
   use y
 ].
 
diff --git a/test/success/pushout.prl b/test/success/pushout.prl
index 6ec57a23a..ecdf5ef80 100644
--- a/test/success/pushout.prl
+++ b/test/success/pushout.prl
@@ -13,7 +13,7 @@ Thm Pushout/Test1 : [
 Thm Pushout/Test2 : [
   (-> dim (pushout bool bool bool [x] x [x] x))
 ] by [
-  <u> `(glue u tt tt tt)
+  abs u => `(glue u tt tt tt)
 ].
 
 Def S1' = [(pushout record record bool [_] tuple [_] tuple)].
@@ -22,7 +22,7 @@ Def S1' = [(pushout record record bool [_] tuple [_] tuple)].
 Thm PushoutToS1 : [
   (-> S1' S1)
 ] by [
-  lam p. fresh a, b, u:dim, c -> elim p;
+  lam p => fresh a b u:dim c -> elim p;
     [ `base
     , `base
     , elim c;
diff --git a/test/success/record.prl b/test/success/record.prl
index e1f0bbad6..d81254ea1 100644
--- a/test/success/record.prl
+++ b/test/success/record.prl
@@ -39,7 +39,7 @@ Thm RecordTest4 : [
 Thm RecordTest5(#p) : [
   (-> [p : record] (= record p tuple))
 ] by [
-  lam _. auto
+  lam _ => auto
 ].
 
 Thm RecordTest6 : [
@@ -47,7 +47,7 @@ Thm RecordTest6 : [
     [p : (record [a : bool] [b c : record])]
     bool)
 ] by [
-  lam {a = a}. use a
+  lam {a = a} => use a
 ].
 
 Thm RecordTest7 : [
@@ -55,7 +55,7 @@ Thm RecordTest7 : [
    [a : S1]
    [b : (path [_] S1 a a)])
 ] by [
-  {a = `base, b = <i> `(loop i)}
+  {a = `base, b = abs i => `(loop i)}
 ].
 
 Thm RecordElimTest : [
@@ -66,7 +66,7 @@ Thm RecordElimTest : [
     [p : (path [_] bool b b)])
    (* [b : bool] (path [_] bool b b)))
 ] by [
-  lam {b = welp, p = hello}.
+  lam {b = welp, p = hello} =>
     {use welp, use hello}
 ].
 
diff --git a/test/success/semi-simplicial.prl b/test/success/semi-simplicial.prl
index 0e05059ae..0e81de522 100644
--- a/test/success/semi-simplicial.prl
+++ b/test/success/semi-simplicial.prl
@@ -2,9 +2,9 @@ Thm Pick : [
   // pick #(first argument) from #(second argument)
   (-> nat nat (U 0))
 ] by [
-  lam n. fresh n', n'/ih -> elim n;
-  [ lam n. `record
-  , lam m. fresh m', m'/ih -> elim m;
+  lam n => fresh n' n'/ih -> elim n;
+  [ lam n => `record
+  , lam m => fresh m' m'/ih -> elim m;
     [ `void
     , `(record
         [head : bool]
@@ -18,13 +18,13 @@ Thm Pick : [
 Thm Pick/zero/L : [
   (-> [n : nat] (= (U 0) ($ Pick zero n) record))
 ] by [
-  lam n. auto
+  lam n => auto
 ].
 
 Thm Pick/succ/0/zero/1 : [
   (-> [n : nat] (= (U 0) ($ Pick (succ n) zero) void))
 ] by [
-  lam n. auto
+  lam n => auto
 ].
 
 Thm Pick/succ/0/succ/1 : [
@@ -35,9 +35,9 @@ Thm Pick/succ/0/succ/1 : [
      [head : bool]
      [tail : (if head ($ Pick n m) ($ Pick (succ n) m))])))
 ] by [
-  lam n, m.
-    let aux0 : [($ Pick n m) type at 0] = auto.
-    let aux1 : [($ Pick (succ n) m) type at 0] = auto.
+  lam n m =>
+    claim aux0 : [($ Pick n m) type at 0] by [auto];
+    claim aux1 : [($ Pick (succ n) m) type at 0] by [auto];
     unfold Pick; reduce; auto
 ].
 
@@ -56,16 +56,16 @@ Thm Pick/compose : [
    ($ Pick a b)
    ($ Pick a c))
 ] by [
-  lam a. fresh a', a'/ih -> elim a;
-  [ lam b, c, p0, p1. `tuple
-  , lam b. fresh b', b'/ih -> elim b;
-    [ lam c, p0, p1. elim p1
-    , lam c. fresh c', c'/ih -> elim c;
-      [ lam p0. elim p0
-      , lam p0. (Replace p0 ($ Pick/succ/0/succ/1 b' c'));
-        let {head = p0/h, tail = p0/t} = p0. elim p0/h;
-        [ lam p1. (Replace p1 ($ Pick/succ/0/succ/1 a' b'));
-          let {head = p1/h, tail = p1/t} = p1. elim p1/h;
+  lam a => fresh a' a'/ih -> elim a;
+  [ lam b c p0 p1 => `tuple
+  , lam b => fresh b' b'/ih -> elim b;
+    [ lam c p0 p1 => elim p1
+    , lam c => fresh c' c'/ih -> elim c;
+      [ lam p0 => elim p0
+      , lam p0 => (Replace p0 ($ Pick/succ/0/succ/1 b' c'));
+        let {head = p0/h, tail = p0/t} = p0; elim p0/h;
+        [ lam p1 => (Replace p1 ($ Pick/succ/0/succ/1 a' b'));
+          let {head = p1/h, tail = p1/t} = p1; elim p1/h;
           (ReplaceGoal ($ Pick/succ/0/succ/1 a' c'));
           [ { head = `tt
             , tail = `($ a'/ih b' c' p0/t p1/t)
@@ -74,7 +74,7 @@ Thm Pick/compose : [
             , tail = `($ b'/ih c' p0/t p1/t)
             }
           ]
-        , lam p1.
+        , lam p1 =>
           (ReplaceGoal ($ Pick/succ/0/succ/1 a' c'));
           { head = `ff
           , tail = `($ c'/ih p0/t p1)
@@ -92,7 +92,7 @@ Thm Pick/compose/zero/0 : [
    [p1 : ($ Pick 0 b)]
    (= ($ Pick 0 c) ($ Pick/compose 0 b c p0 p1) tuple))
 ] by [
-  lam a, b, p0, p1. auto
+  lam a b p0 p1 => auto
 ].
 
 Thm Pick/compose/tt/4/0/tt/5/0 : [
@@ -106,13 +106,14 @@ Thm Pick/compose/tt/4/0/tt/5/0 : [
        (tuple [head tt] [tail p0/t]) (tuple [head tt] [tail p1/t]))
     (tuple [head tt] [tail ($ Pick/compose a b c p0/t p1/t)])))
 ] by [
-  lam a, b, c, p0/t, p1/t.
-    let aux0 :
+  lam a b c p0/t p1/t =>
+    claim aux0 :
       [  ($ Pick/compose a b c (! tail (tuple [head tt] [tail p0/t])) (! tail (tuple [head tt] [tail p1/t])))
       =  ($ Pick/compose a b c p0/t p1/t)
-      in ($ Pick a c) ] = auto.
-    let aux1 : [ ($ Pick (succ a) c) type at 0 ] = auto.
-    unfold [Pick, Pick/compose]; reduce; auto
+      in ($ Pick a c)
+      ] by [auto];
+    claim aux1 : [ ($ Pick (succ a) c) type at 0 ] by [auto];
+      unfold Pick Pick/compose; reduce; auto
 ].
 
 Thm Pick/compose/tt/4/0/ff/5/0 : [
@@ -126,13 +127,14 @@ Thm Pick/compose/tt/4/0/ff/5/0 : [
        (tuple [head tt] [tail p0/t]) (tuple [head ff] [tail p1/t]))
     (tuple [head ff] [tail ($ Pick/compose (succ a) b c p0/t p1/t)])))
 ] by [
-  lam a, b, c, p0/t, p1/t.
-    let aux0 :
+  lam a b c p0/t p1/t =>
+    claim aux0 :
       [  ($ Pick/compose (succ a) b c (! tail (tuple [head tt] [tail p0/t])) (! tail (tuple [head ff] [tail p1/t])))
       =  ($ Pick/compose (succ a) b c p0/t p1/t)
-      in ($ Pick (succ a) c) ] = auto.
-    let aux1 : [ ($ Pick a c) type at 0 ] = auto.
-    unfold [Pick, Pick/compose]; reduce; auto
+      in ($ Pick (succ a) c)
+      ] by [auto];
+    claim aux1 : [ ($ Pick a c) type at 0 ] by [auto];
+    unfold Pick Pick/compose; reduce; auto
 ].
 
 Thm Pick/compose/ff/4/0 : [
@@ -146,11 +148,12 @@ Thm Pick/compose/ff/4/0 : [
        (tuple [head ff] [tail p0/t]) p1)
     (tuple [head ff] [tail ($ Pick/compose (succ a) (succ b) c p0/t p1)])))
 ] by [
-  lam a, b, c, p0/t, p1.
-    let aux0 :
+  lam a b c p0/t p1 =>
+    claim aux0 :
       [  ($ Pick/compose (succ a) (succ b) c (! tail (tuple [head ff] [tail p0/t])) p1)
       =  ($ Pick/compose (succ a) (succ b) c p0/t p1)
-      in ($ Pick (succ a) c) ] = auto.
-    let aux1 : [ ($ Pick a c) type at 0 ] = auto.
-    unfold [Pick, Pick/compose]; reduce; auto
+      in ($ Pick (succ a) c)
+      ] by [auto];
+    claim aux1 : [ ($ Pick a c) type at 0 ] by [auto];
+    unfold Pick Pick/compose; reduce; auto
 ].
diff --git a/test/success/strict-bool.prl b/test/success/strict-bool.prl
index e27e21be6..3e8fc9078 100644
--- a/test/success/strict-bool.prl
+++ b/test/success/strict-bool.prl
@@ -18,7 +18,7 @@ Thm SBool/Not-Not-Id-Path : [
     (Cmp Bool/Not Bool/Not)
     (lam [x] x))
 ] by [
-  <i> lam x. use x
+  abs i => lam x => use x
 ].
 
 Extract SBool/Not-Not-Id-Path.
diff --git a/test/success/theorem-of-choice.prl b/test/success/theorem-of-choice.prl
index b0de99293..1897d18c2 100644
--- a/test/success/theorem-of-choice.prl
+++ b/test/success/theorem-of-choice.prl
@@ -7,9 +7,9 @@ Thm Choice(#i:lvl) : [
     [f : (-> a b)]
     (-> [x : a] ($ r x ($ f x)))))
 ] by [
-  lam a, b, r, f.
-    {lam x. let {y,_} = f [`x]. `y,
-     lam x. let {_,z} = f [`x]. `z};
+  lam a b r f =>
+    {lam x => let {y,_} = f [`x]; `y,
+     lam x => let {_,z} = f [`x]; `z};
     inversion; reduce; auto
 ].
 
diff --git a/test/success/unfold.prl b/test/success/unfold.prl
index 566539c38..7872d1ed1 100644
--- a/test/success/unfold.prl
+++ b/test/success/unfold.prl
@@ -3,19 +3,19 @@ Def Times(#A, #B) = [
 ].
 
 Tac Proj1(#z) = [
-  let {x} = #z.
+  let {x} = #z;
   use x
 ].
 
 Tac Proj2(#z) = [
-  let {welp, x} = #z.
+  let {welp, x} = #z;
   use x
 ].
 
 Thm Times/Proj : [
   (-> [ty : (U 0)] (Times bool ty) ty)
 ] by [
-  lam ty, x. (Proj2 x)
+  lam ty x => (Proj2 x)
 ].
 
 Extract Times/Proj.
diff --git a/test/success/wbool-fhcom.prl b/test/success/wbool-fhcom.prl
index c419b00dd..162611be1 100644
--- a/test/success/wbool-fhcom.prl
+++ b/test/success/wbool-fhcom.prl
@@ -4,7 +4,7 @@ Thm WBoolSym : [
    (path [_] wbool a b)
    (path [_] wbool b a))
 ] by [
-  lam a, b, p. <i> 
+  lam a b p => abs i =>
      `(hcom 0~>1 wbool a [i=0 [j] (@ p j)] [i=1 [_] a])
 ].
 
diff --git a/test/wip/ua.prl b/test/wip/ua.prl
index 53b01ba8d..d5136a3e4 100644
--- a/test/wip/ua.prl
+++ b/test/wip/ua.prl
@@ -15,10 +15,10 @@ Def IsProp (#C) = [(-> [c c' : #C] (path [_] #C c c'))].
 Def IsSet (#C) = [(-> [c c' : #C] (IsProp (path [_] #C c c')))].
 
 Tac ReflectUniv(#l:lvl, #k:knd, #t:tac) = [
-  query goal <- concl.
+  query goal <- concl;
   match goal {
-    [a, b, k, l | #jdg{%a = %b type at %l with %[k:knd]} =>
-      let aux : [%a = %b in (U #l #k)] = #t. auto
+    [a b k l | #jdg{%a = %b type at %l with %[k:knd]} =>
+      claim aux : [%a = %b in (U #l #k)] by [#t]; auto
     ]
   }
 ].
@@ -32,15 +32,16 @@ Tac CrushTyEq(#l:lvl) = [
 Thm IdIsEquiv(#l:lvl) : [
   (-> [ty : (U #l hcom)] (IsEquiv ty ty Id))
 ] by [
-  lam ty, a.
-  { {use a, <_> use a}
-  , lam {_,c'}. <i>
+  lam ty a =>
+  { {use a, abs _ => use a}
+  , lam {_,c'} => abs i =>
        { `(hcom 1~>0 ty a
            [i=0 [j] (@ c' j)]
            [i=1 [j] a])
-       , <j> `(hcom 1~>j ty a
-               [i=0 [j] (@ c' j)]
-               [i=1 [j] a])
+       , abs j =>
+           `(hcom 1~>j ty a
+             [i=0 [j] (@ c' j)]
+             [i=1 [j] a])
        }
   }
 ].
@@ -48,7 +49,7 @@ Thm IdIsEquiv(#l:lvl) : [
 Thm IdEquiv(#l:lvl) : [
   (-> [ty : (U #l hcom)] (Equiv ty ty))
 ] by [
-  lam ty.
+  lam ty =>
     {`Id, use (IdIsEquiv #l) [use ty]}
 ].
 
@@ -57,8 +58,8 @@ Thm UA(#l:lvl) : [
       [e : (Equiv ty/a ty/b)]
       (path [_] (U #l kan) ty/a ty/b))
 ] by [
-  lam ty/a, ty/b, e.
-    <x> `(V x ty/a ty/b e)
+  lam ty/a ty/b e =>
+    abs x => `(V x ty/a ty/b e)
 ].
 
 Thm UABeta(#l:lvl) : [
@@ -71,8 +72,8 @@ Thm UABeta(#l:lvl) : [
     ($ (!proj1 e) a)))
 ] by [
   unfold UA;
-  lam ty/a, ty/b, e, a.
-    <x> `(coe x~>1 [_] ty/b ($ (! proj1 e) a))
+  lam ty/a ty/b e a =>
+    abs x => `(coe x~>1 [_] ty/b ($ (! proj1 e) a))
 ].
 
 // coe{0~>1} is an equivalence
@@ -83,7 +84,7 @@ Thm PathToEquiv(#l:lvl) : [
    [p : (path [_] (U #l kan) ty/a ty/b)]
    (Equiv ty/a ty/b))
 ] by [
-  lam ty/a, ty/b, p.
+  lam ty/a ty/b p =>
   `(coe 0~>1 [x] (Equiv ty/a (@ p x)) ($ (IdEquiv #l) ty/a));
   (CrushTyEq #l)
 ].
@@ -94,21 +95,21 @@ Thm PathToEquiv(#l:lvl) : [
 //    [p : (path [_] (U #l kan) ty/a ty/b)]
 //    (Equiv ty/a ty/b))
 // ] by [
-//   unfold [Equiv, IsEquiv, IsContr, Fiber, HasAllPathsTo];
-//   lam ty/a, ty/b, p.
-//   { lam a.
+//   unfold Equiv IsEquiv IsContr Fiber HasAllPathsTo;
+//   lam ty/a ty/b p =>
+//   { lam a =>
 //       `(coe 0~>1 [i] (@ p i) a); (CrushTyEq #l)
-//   , lam b.
+//   , lam b =>
 //       {
 //         { `(coe 1~>0 [i] (@ p i) b)
 //         , <x> `(coe x~>1 [i] (@ p i) (coe 1~>x [i] (@ p i) b))
 //         }; (CrushTyEq #l)
-//       , lam c. <x>
+//       , lam c => abs x =>
 //         { `(com 1~>0 [i] (@ p i) (@ (!proj2 c) x)
 //              [x=0 [z] (coe 0~>z [i] (@ p i) (!proj1 c))]
 //              [x=1 [z] (coe 1~>z [i] (@ p i) b)]);
 //           (CrushTyEq #l)
-//         , <y> ?foo
+//         , abs y => ?foo
 //         }
 //       }
 //   }
@@ -129,7 +130,7 @@ Thm LemPropF(#l:lvl) : [
    (path [x] ($ ty/b (@ p x)) b0 b1))
 ] by [
   unfold IsProp;
-  lam ty/a, ty/b, prop/b, a0, a1, p, b0, b1. <x>
+  lam ty/a ty/b prop/b a0 a1 p b0 b1 => abs x =>
   `(@ ($ prop/b (@ p x) (coe 0~>x [i] ($ ty/b (@ p i)) b0) (coe 1~>x [i] ($ ty/b (@ p i)) b1)) x)
 ].
 
@@ -142,7 +143,7 @@ Thm LemSig(#l:lvl) : [
    [p : (path [_] ty/a (!proj1 u) (!proj1 v))]
    (path [_] (* [a : ty/a] ($ ty/b a)) u v))
 ] by [
-  lam ty/a, ty/b, prop/b, {u1, u2}, {v1, v2}, p. <x>
+  lam ty/a ty/b prop/b {u1, u2} {v1, v2} p => abs x =>
   {`(@ p x), `(@ ($ (LemPropF #l) ty/a ty/b prop/b u1 v1 p u2 v2) x)}
 ].
 
@@ -156,7 +157,7 @@ Thm PropSig(#l:lvl) : [
    (path [_] (* [a : ty/a] ($ ty/b a)) u v))
 ] by [
   unfold IsProp;
-  lam ty/a, ty/b, prop/a, prop/b, u, v.
+  lam ty/a ty/b prop/a prop/b u v =>
   `($ (LemSig #l) ty/a ty/b prop/b u v ($ prop/a (!proj1 u) (!proj1 v)))
 ].
 
@@ -169,8 +170,8 @@ Thm PropPi(#l:lvl) : [
    (path [_] (-> [a : ty/a] ($ ty/b a)) f g))
 ] by [
   unfold IsProp;
-  lam ty/a, ty/b, prop/b, f, g.
-  <x> lam a. `(@ ($ prop/b a ($ f a) ($ g a)) x)
+  lam ty/a ty/b prop/b f g =>
+  abs x => lam a => `(@ ($ prop/b a ($ f a) ($ g a)) x)
 ].
 
 Thm LemProp(#l:lvl) : [
@@ -181,8 +182,8 @@ Thm LemProp(#l:lvl) : [
   (IsContr ty/a))
 ] by [
   unfold IsProp;
-  lam ty/a, prop/a, a.
-  {`a , lam a'. `($ prop/a a' a)}
+  lam ty/a prop/a a =>
+  {`a , lam a' => `($ prop/a a' a)}
 ].
 
 Thm PropSet(#l:lvl) : [
@@ -191,9 +192,9 @@ Thm PropSet(#l:lvl) : [
    [prop : (IsProp ty)]
    (IsSet ty))
 ] by [
-  unfold [IsProp, IsSet];
-  lam ty, prop.
-  lam a, b, p, q. <x y>
+  unfold IsProp IsSet;
+  lam ty prop =>
+  lam a b p q => abs x y =>
   `(hcom 0~>1 ty a
      [y=0 [z] (@ ($ prop a a) z)]
      [y=1 [z] (@ ($ prop a b) z)]
@@ -206,26 +207,28 @@ Thm PropIsContr(#l:lvl) : [
    [ty/a : (U #l kan)]
    (IsProp (IsContr ty/a)))
 ] by [
-  lam ty/a.
-  let fun : [(-> (IsContr ty/a) (IsProp (IsContr ty/a)))] =
-    lam contr/a.
-    let prop/a : [(IsProp ty/a)] =
-      (lam a, a'. <x>
-      `(hcom 1~>0 ty/a (@ ($ (!proj2 contr/a) a) x)
+  lam ty/a =>
+  claim fun : [(-> (IsContr ty/a) (IsProp (IsContr ty/a)))] by [
+    lam contr/a =>
+    claim prop/a : [(IsProp ty/a)] by [
+      (lam a a' => abs x =>
+       `(hcom 1~>0 ty/a (@ ($ (!proj2 contr/a) a) x)
          [x=0 [_] a]
-         [x=1 [y] (@ ($ (!proj2 contr/a) a') y)])).
+         [x=1 [y] (@ ($ (!proj2 contr/a) a') y)]))
+    ];
     let prop/contr/a = (PropSig #l)
       [`ty/a,
-       lam a. `(-> [a' : ty/a] (path [_] ty/a a' a)),
+       lam a => `(-> [a' : ty/a] (path [_] ty/a a' a)),
        `prop/a,
-       lam a.
+       lam a =>
          `($ (PropPi #l)
              ty/a
              (lam [a'] (path [_] ty/a a' a))
              (lam [a'] ($ (PropSet #l) ty/a prop/a a' a)))
-      ].
-    `prop/contr/a.
-  lam x. `($ fun x x)
+      ];
+    `prop/contr/a
+  ];
+  lam x => `($ fun x x)
 ].
 
 // try to write PropIsEquivDirect
@@ -235,8 +238,8 @@ Thm PropIsEquiv(#l:lvl) : [
    [f : (-> ty/a ty/b)]
    (IsProp (IsEquiv ty/a ty/b f)))
 ] by [
-  lam ty/a, ty/b, f.
-  lam e0, e1. <x> lam b.
+  lam ty/a ty/b f =>
+  lam e0 e1 => abs x => lam b =>
   `(@ ($ (PropIsContr #l) (Fiber ty/a ty/b f b) ($ e0 b) ($ e1 b)) x)
 ].
 
@@ -247,7 +250,7 @@ Thm EquivLemma(#l:lvl) : [
    (path [_] (-> ty/a ty/b) (!proj1 e1) (!proj1 e2))
    (path [_] (Equiv ty/a ty/b) e1 e2))
 ] by [
-  lam ty/a, ty/b.
+  lam ty/a ty/b =>
   `($ (LemSig #l)
       (-> ty/a ty/b)
       (lam [f] (IsEquiv ty/a ty/b f))
@@ -261,7 +264,7 @@ Thm Retract(#l:lvl) : [
    [g : (-> ty/b ty/a)]
    (U #l kan))
 ] by [
-  lam ty/a, ty/b, f, g.
+  lam ty/a ty/b f g =>
     `(-> [a : ty/a] (path [_] ty/a ($ g ($ f a)) a))
 ].
 
@@ -274,7 +277,7 @@ Thm UARet(#l:lvl) : [
       ($ (UA #l) ty/a ty/b)
       ($ (PathToEquiv #l) ty/a ty/b)))
 ] by [
-  lam ty/a, ty/b, e.
+  lam ty/a ty/b e =>
   `($ (EquivLemma #l) ty/a ty/b
       ($ (PathToEquiv #l) ty/a ty/b ($ (UA #l) ty/a ty/b e))
       e
@@ -287,11 +290,11 @@ Thm IsContrPath(#l:lvl) : [
    [ty/a : (U #l kan)]
    (IsContr (* [ty/b : (U #l kan)] (path [_] (U #l kan) ty/a ty/b))))
 ] by [
-  lam ty/a.
-  {{use ty/a, <_> use ty/a},
-   lam {ty/b,p}. <x>
+  lam ty/a =>
+  {{use ty/a, abs _ => use ty/a},
+   lam {ty/b,p} => abs x =>
      {`(hcom 0~>1 (U #l kan) ty/a [x=0 [y] (@ p y)] [x=1 [_] ty/a]),
-      <y> `(hcom 0~>y (U #l kan) ty/a [x=0 [y] (@ p y)] [x=1 [_] ty/a])}
+      abs y => `(hcom 0~>y (U #l kan) ty/a [x=0 [y] (@ p y)] [x=1 [_] ty/a])}
   };
   auto; (CrushTyEq #l)
 ].
@@ -305,9 +308,9 @@ Thm RetIsContr(#l:lvl) : [
    [contr/b : (IsContr ty/b)]
    (IsContr ty/a))
 ] by [
-  lam ty/a, ty/b, f, g, h, {b,p}.
+  lam ty/a ty/b f g h {b,p} =>
   {`($ g b),
-   lam a. <x>
+   lam a => abs x =>
      `(hcom 0~>1 ty/a ($ g (@ ($ p ($ f a)) x))
         [x=0 [y] (@ ($ h a) y)]
         [x=1 [_] ($ g b)])}
@@ -319,8 +322,8 @@ Thm SigEquivToPath(#l:lvl) : [
    (* [ty/b : (U #l kan)] (Equiv ty/a ty/b))
    (* [ty/b : (U #l kan)] (path [_] (U #l kan) ty/a ty/b)))
 ] by [
-  lam ty/a, {ty/b,equiv}.
-  {use ty/b, <x> `(V x ty/a ty/b equiv)}
+  lam ty/a {ty/b,equiv} =>
+  {use ty/b, abs x => `(V x ty/a ty/b equiv)}
 ].
 
 Thm SigPathToEquiv(#l:lvl) : [
@@ -329,7 +332,7 @@ Thm SigPathToEquiv(#l:lvl) : [
    (* [ty/b : (U #l kan)] (path [_] (U #l kan) ty/a ty/b))
    (* [ty/b : (U #l kan)] (Equiv ty/a ty/b)))
 ] by [
-  lam ty/a, {ty/b,p}.
+  lam ty/a {ty/b,p} =>
   {use ty/b, `($ (PathToEquiv #l) ty/a ty/b p)}
 ].
 
@@ -342,9 +345,9 @@ Thm UARetSig(#l:lvl) : [
       ($ (SigEquivToPath #l) ty/a)
       ($ (SigPathToEquiv #l) ty/a)))
 ] by [
-  (lam ty/a, {ty/b,equiv}. <x>
+  (lam ty/a {ty/b,equiv} => abs x =>
   {use ty/b, ?});
-  unfold [PathToEquiv, SigPathToEquiv, SigEquivToPath];
+  unfold PathToEquiv SigPathToEquiv SigEquivToPath;
   [id,?, id]
   // {use ty/b, `(@ ($ (UARet #l) ty/a ty/b equiv) x)}
 ].
@@ -354,14 +357,14 @@ Thm UARetSig(#l:lvl) : [
 //    [ty/a : (U #l kan)]
 //    (IsContr (* [ty/b : (U #l kan)] (Equiv ty/a ty/b))))
 // ] by [
-//   lam ty/a.
-//   let contr = (RetIsContr #lvl{(++ #l)})
+//   lam ty/a =>
+//   let contr = (RetIsContr (++ #l))
 //     [`(* [ty/b : (U #l kan)] (Equiv ty/a ty/b)),
 //      `(* [ty/b : (U #l kan)] (path [_] (U #l kan) ty/a ty/b)),
 //      `($ (SigEquivToPath #l) ty/a),
 //      `($ (SigPathToEquiv #l) ty/a),
 //      `($ (UARetSig #l) ty/a),
-//      `($ (IsContrPath #l) ty/a)].
+//      `($ (IsContrPath #l) ty/a)];
 //   use contr
 // ].