diff --git a/prelude.m31 b/prelude.m31
index 5b5a81bb..88f2bc6b 100644
--- a/prelude.m31
+++ b/prelude.m31
@@ -2,8 +2,8 @@
 #include_once "std/base.m31"
 #include_once "std/equal.m31"
 
-let top_betas = nil
-let top_hints = nil
-let top_action = reset
+let top_betas = ref []
+let top_hints = ref []
+let top_action = ref reset
 
 #include "std/equal_handle.m31"
diff --git a/src/nucleus/eval.ml b/src/nucleus/eval.ml
index bb08e880..d8b4226f 100644
--- a/src/nucleus/eval.ml
+++ b/src/nucleus/eval.ml
@@ -36,6 +36,10 @@ let as_ref ~loc v =
   let e = Value.as_ref ~loc v in
   Value.return e
 
+let as_list ~loc v =
+  let lst = Value.as_list ~loc v in
+  Value.return lst
+
 (** Evaluate a computation -- infer mode. *)
 let rec infer env (c',loc) =
   match c' with
@@ -75,6 +79,14 @@ let rec infer env (c',loc) =
        in
        fold [] cs
 
+    | Syntax.Nil ->
+       Value.return Value.list_nil
+
+    | Syntax.Cons (c1, c2) ->
+       infer env c1 >>= fun v1 ->
+       infer env c2 >>= as_list ~loc >>= fun lst ->
+       Value.return (Value.list_cons v1 lst)
+
     | Syntax.Handler {Syntax.handler_val; handler_ops; handler_finally} ->
         let handler_val =
           begin match handler_val with
@@ -254,7 +266,7 @@ let rec infer env (c',loc) =
               Value.apply_closure env f >>= fun v ->
               fold v cs
           end
-        | Value.Ty _ | Value.Handler _ | Value.Tag _ | Value.Ref _ ->
+        | Value.Ty _ | Value.Handler _ | Value.Tag _ | Value.List _ | Value.Ref _ ->
           Error.runtime ~loc "cannot apply %s" (Value.name_of v)
     in
     infer env c >>= fun v -> fold v cs
@@ -374,6 +386,8 @@ and check env ((c',loc) as c) (((ctx_check, t_check') as t_check) : Judgement.ty
   | Syntax.Handler _
   | Syntax.External _
   | Syntax.Tag _
+  | Syntax.Nil
+  | Syntax.Cons _
   | Syntax.Where _
   | Syntax.With _
   | Syntax.Typeof _
diff --git a/src/nucleus/value.ml b/src/nucleus/value.ml
index 8fbb4edd..75a852d9 100644
--- a/src/nucleus/value.ml
+++ b/src/nucleus/value.ml
@@ -24,6 +24,7 @@ type value =
   | Closure of (value,value) closure
   | Handler of handler
   | Tag of Name.ident * value list
+  | List of value list
   | Ref of value ref
 
 and ('a,'b) closure = dynamic -> 'a -> 'b result
@@ -86,6 +87,8 @@ and print_value ?max_level xs v ppf =
   | Closure f -> print_closure xs f ppf
   | Handler h -> print_handler xs h ppf
   | Tag (t, lst) -> print_tag ?max_level xs t lst ppf
+  | List lst -> Print.print ~at_level:0 ppf "[%t]"
+                            (Print.sequence (print_value ~max_level:2 xs) "," lst)
   | Ref v -> Print.print ?max_level ~at_level:1 ppf "ref@ %t" (print_value ~max_level:0 xs (!v))
 
 let name_of v =
@@ -95,67 +98,71 @@ let name_of v =
     | Closure _ -> "a function"
     | Handler _ -> "a handler"
     | Tag _ -> "a data tag"
+    | List _ -> "a list"
     | Ref _ -> "a reference"
 
 let as_term ~loc = function
   | Term e -> e
-  | (Ty _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+  | (Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_ty ~loc = function
   | Ty t -> t
-  | (Term _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+  | (Term _ | Closure _ | Handler _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_closure ~loc = function
   | Closure f -> f
-  | (Ty _ | Term _ | Handler _ | Tag _ | Ref _) as v ->
+  | (Ty _ | Term _ | Handler _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_handler ~loc = function
   | Handler h -> h
-  | (Ty _ | Term _ | Closure _ | Tag _ | Ref _) as v ->
+  | (Ty _ | Term _ | Closure _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let as_ref ~loc = function
   | Ref v -> v
-  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _) as v ->
+  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _ | List _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
 let name_some = Name.make "Some"
 let name_none = Name.make "None"
 let name_pair = Name.make "pair"
-let name_cons = Name.make "cons"
-let name_nil = Name.make "nil"
 let name_unit = Name.make "tt"
 
 let predefined_tags = [
   (name_some, 1);
   (name_none, 0);
   (name_pair, 2);
-  (name_cons, 2);
-  (name_nil, 0);
   (name_unit, 0);
 ]
 
 let as_option ~loc = function
   | Tag (t,[]) when (Name.eq_ident t name_none)  -> None
   | Tag (t,[x]) when (Name.eq_ident t name_some) -> Some x
-  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _ | List _ | Ref _) as v ->
     Error.runtime ~loc "expected a term but got %s" (name_of v)
 
+let as_list ~loc = function
+  | List lst -> lst
+  | (Ty _ | Term _ | Closure _ | Handler _ | Tag _ | Ref _) as v ->
+    Error.runtime ~loc "expected a list but got %s" (name_of v)
+
 let from_option = function
   | None -> Tag (name_none, [])
   | Some v -> Tag (name_some, [v])
 
 let from_pair (v1, v2) = Tag (name_pair, [v1; v2])
 
-let rec from_list = function
-  | [] -> Tag (name_nil, [])
-  | v :: vs -> Tag (name_cons, [v; from_list vs])
+let from_list lst = List lst
 
 let mk_tag t lst = Tag (t, lst)
 
+let list_nil = List []
+
+let list_cons v lst = List (v :: lst)
+
 let return x = Return x
 
 let return_term e = Return (Term e)
@@ -233,6 +240,14 @@ let rec equal_value v1 v2 =
         in
       fold vs1 vs2
 
+    | List lst1, List lst2 ->
+       let rec fold = function
+         | [], [] -> true
+         | v1 :: lst1, v2 :: lst2 -> equal_value v1 v2 && fold (lst1, lst2)
+         | [], _::_ | _::_, [] -> false
+       in
+       fold (lst1, lst2)
+
     | Ref v1, Ref v2 ->
        (* XXX should we compare references by value instead? *)
        v1 == v2
@@ -242,12 +257,13 @@ let rec equal_value v1 v2 =
        (* XXX should we use physical comparison == instead? *)
        false
 
-    | Term _, (Ty _ | Closure _ | Handler _ | Tag _ | Ref _)
-    | Ty _, (Term _ | Closure _ | Handler _ | Tag _ | Ref _)
-    | Closure _, (Term _ | Ty _ | Handler _ | Tag _ | Ref _)
-    | Handler _, (Term _ | Ty _ | Closure _ | Tag _ | Ref _)
-    | Tag _, (Term _ | Ty _ | Closure _ | Handler _ | Ref _)
-    | Ref _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _) ->
+    | Term _, (Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Ty _, (Term _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Closure _, (Term _ | Ty _ | Handler _ | Tag _ | List _ | Ref _)
+    | Handler _, (Term _ | Ty _ | Closure _ | Tag _ | List _ | Ref _)
+    | Tag _, (Term _ | Ty _ | Closure _ | Handler _ | List _ | Ref _)
+    | List _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | Ref _)
+    | Ref _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | List _) ->
       false
 
 let (>>=) = bind
@@ -705,8 +721,16 @@ module Env = struct
     | Syntax.Patt_Tag (tag, ps), Tag (tag', vs) when Name.eq_ident tag tag' ->
       multicollect_pattern env xvs ps vs
 
-    | Syntax.Patt_Jdg _, (Ty _ | Closure _ | Handler _ | Tag _ | Ref _)
-    | Syntax.Patt_Tag _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | Ref _) ->
+    | Syntax.Patt_Nil, List [] -> xvs
+
+    | Syntax.Patt_Cons (p1, p2), List (v1 :: v2) ->
+       let xvs = collect_pattern env xvs p1 v1 in
+       collect_pattern env xvs p2 (List v2)
+
+    | Syntax.Patt_Nil, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Syntax.Patt_Cons _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Syntax.Patt_Jdg _, (Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _)
+    | Syntax.Patt_Tag _, (Term _ | Ty _ | Closure _ | Handler _ | Tag _ | List _ | Ref _) ->
        raise Match_fail
 
   and multicollect_pattern env xvs ps vs =
diff --git a/src/nucleus/value.mli b/src/nucleus/value.mli
index 15133048..2b36e7ea 100644
--- a/src/nucleus/value.mli
+++ b/src/nucleus/value.mli
@@ -21,6 +21,7 @@ type value = private
   | Closure of (value,value) closure
   | Handler of handler
   | Tag of Name.ident * value list
+  | List of value list
   | Ref of value ref
 
 and ('a,'b) closure
@@ -61,8 +62,11 @@ val from_list : value list -> value
 
 (** Convert tags to ocaml types *)
 val as_option : loc:Location.t -> value -> value option
+val as_list : loc:Location.t -> value -> value list
 
 val mk_tag : Name.ident -> value list -> value
+val list_nil : value
+val list_cons : value -> value list -> value
 
 val return : 'a -> 'a result
 val return_term : Judgement.term -> value result
diff --git a/src/parser/desugar.ml b/src/parser/desugar.ml
index cf2b893a..3342b037 100644
--- a/src/parser/desugar.ml
+++ b/src/parser/desugar.ml
@@ -218,7 +218,7 @@ let rec pattern (env : Value.Env.t) bound vars n (p,loc) =
       let p2, vars, n = tt_pattern env bound vars n p2 in
       (Syntax.Patt_Jdg (p1,p2), loc), vars, n
 
-    | Input.Patt_Data (t,ps) ->
+    | Input.Patt_Tag (t,ps) ->
       let rec fold vars n ps = function
         | [] ->
           let ps = List.rev ps in
@@ -229,6 +229,20 @@ let rec pattern (env : Value.Env.t) bound vars n (p,loc) =
         in
       fold vars n [] ps
 
+    | Input.Patt_Cons (p1, p2) ->
+      let p1, vars, n = pattern env bound vars n p1 in
+      let p2, vars, n = pattern env bound vars n p2 in
+      (Syntax.Patt_Cons (p1,p2), loc), vars, n
+
+    | Input.Patt_List ps ->
+       let rec fold ~loc vars n = function
+         | [] -> (Syntax.Patt_Nil, loc), vars, n
+         | p :: ps ->
+            let p, vars, n = pattern env bound vars n p in
+            let ps, vars, n = fold ~loc:(snd p) vars n ps in
+            (Syntax.Patt_Cons (p, ps), loc), vars, n
+       in
+       fold ~loc vars n ps
 
 let rec comp ~yield (env : Value.Env.t) bound (c',loc) =
   match c' with
@@ -461,6 +475,21 @@ let rec comp ~yield (env : Value.Env.t) bound (c',loc) =
      let cs = List.map (comp ~yield env bound) cs in
      Syntax.Tag (t, cs), loc
 
+  | Input.List cs ->
+     let rec fold ~loc = function
+       | [] -> Syntax.Nil, loc
+       | c :: cs ->
+          let c = comp ~yield env bound c in
+          let cs = fold ~loc:(snd c) cs in
+          Syntax.Cons (c, cs), loc
+     in
+     fold ~loc cs
+
+  | Input.Cons (e1, e2) ->
+    let e1 = comp ~yield env bound e1 in
+    let e2 = comp ~yield env bound e2 in
+    Syntax.Cons (e1,e2), loc
+
   | Input.Congruence (e1,e2) ->
     let e1 = comp ~yield env bound e1 in
     let e2 = comp ~yield env bound e2 in
diff --git a/src/parser/input.mli b/src/parser/input.mli
index 4d3c57e6..9c4c90f3 100644
--- a/src/parser/input.mli
+++ b/src/parser/input.mli
@@ -30,7 +30,9 @@ and pattern' =
   | Patt_Var of Name.ident
   | Patt_Name of Name.ident
   | Patt_Jdg of tt_pattern * tt_pattern
-  | Patt_Data of Name.ident * pattern list
+  | Patt_Tag of Name.ident * pattern list
+  | Patt_Cons of pattern * pattern
+  | Patt_List of pattern list
 
 (** Sugared terms *)
 type term = term' * Location.t
@@ -45,6 +47,8 @@ and term' =
   | Handle of comp * handle_case list
   | With of expr * comp
   | Tag of Name.ident * comp list
+  | Cons of comp * comp
+  | List of comp list
   | Match of comp * match_case list
   | Let of (Name.ident * comp) list * comp
   | Lookup of comp
diff --git a/src/parser/lexer.ml b/src/parser/lexer.ml
index 763c5d1b..b3173f4a 100644
--- a/src/parser/lexer.ml
+++ b/src/parser/lexer.ml
@@ -97,10 +97,13 @@ and token_aux ({ stream;_ } as lexbuf) =
   | quoted_string            -> f (); let s = lexeme lexbuf in QUOTED_STRING (String.sub s 1 (String.length s - 2))
   | '('                      -> f (); LPAREN
   | ')'                      -> f (); RPAREN
+  | '['                      -> f (); LBRACK
+  | ']'                      -> f (); RBRACK
   | '{'                      -> f (); LBRACE
   | '}'                      -> f (); RBRACE
   | "="                      -> f (); EQ
   | ':'                      -> f (); COLON
+  | "::"                     -> f (); COLONCOLON
   | ','                      -> f (); COMMA
   | '?', name                -> f (); PATTVAR (let s = lexeme lexbuf in String.sub s 1 (String.length s - 1))
   | '.', name                -> f (); PROJECTION (let s = lexeme lexbuf in String.sub s 1 (String.length s - 1))
diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index 86bb47bf..313e9348 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -32,7 +32,8 @@
 (* Parentheses & punctuations *)
 %token LPAREN RPAREN
 %token LBRACE RBRACE
-%token COLON COMMA
+%token LBRACK RBRACK
+%token COLON COLONCOLON COMMA
 %token ARROW DARROW
 
 (* Things specific to toplevel *)
@@ -82,6 +83,7 @@
 %nonassoc COLONEQ
 %left     INFIXOP0
 %right    INFIXOP1
+%right    COLONCOLON
 %left     INFIXOP2
 %left     INFIXOP3
 %right    INFIXOP4
@@ -167,6 +169,7 @@ binop_term: mark_location(plain_binop_term) { $1 }
 plain_binop_term:
   | e=plain_app_term                                { e }
   | e1=app_term COLONEQ e2=binop_term               { Update (e1, e2) }
+  | e1=binop_term COLONCOLON e2=binop_term          { Cons (e1, e2) }
   | e2=binop_term op=INFIXOP0 e3=binop_term
     { let e1 = Var (Name.make ~fixity:Name.Infix0 (fst op)), snd op in Spine (e1, [e2; e3]) }
   | e2=binop_term op=INFIXOP1 e3=binop_term
@@ -203,6 +206,7 @@ plain_simple_term:
   | TYPE                                            { Type }
   | x=var_name                                      { Var x }
   | EXTERNAL s=QUOTED_STRING                        { External s }
+  | LBRACK lst=separated_list(COMMA, equal_term) RBRACK { List lst }
   | LPAREN e=plain_term RPAREN                      { e }
   | LBRACE lst=separated_list(COMMA, signature_clause) RBRACE
         { Signature lst }
@@ -330,32 +334,35 @@ binop_pattern: mark_location(plain_binop_pattern) { $1 }
 plain_binop_pattern:
   | e=plain_app_pattern                                { e }
   | e1=binop_pattern op=INFIXOP0 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix0 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix0 (fst op) in Patt_Tag (op, [e1; e2]) }
   | e1=binop_pattern op=INFIXOP1 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix1 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix1 (fst op) in Patt_Tag (op, [e1; e2]) }
+  | e1=binop_pattern COLONCOLON  e2=binop_pattern
+    { Patt_Cons (e1, e2) }
   | e1=binop_pattern op=INFIXOP2 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix2 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix2 (fst op) in Patt_Tag (op, [e1; e2]) }
   | e1=binop_pattern op=INFIXOP3 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix3 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix3 (fst op) in Patt_Tag (op, [e1; e2]) }
   | e1=binop_pattern op=INFIXOP4 e2=binop_pattern
-    { let op = Name.make ~fixity:Name.Infix4 (fst op) in Patt_Data (op, [e1; e2]) }
+    { let op = Name.make ~fixity:Name.Infix4 (fst op) in Patt_Tag (op, [e1; e2]) }
 
 (* app_pattern: mark_location(plain_app_pattern) { $1 } *)
 plain_app_pattern:
   | e=plain_prefix_pattern                    { e }
-  | t=var_name ps=prefix_pattern+             { Patt_Data (t, ps) }
+  | t=var_name ps=prefix_pattern+             { Patt_Tag (t, ps) }
 
 prefix_pattern: mark_location(plain_prefix_pattern) { $1 }
 plain_prefix_pattern:
   | e=plain_simple_pattern           { e }
-  | op=PREFIXOP e=prefix_pattern     { let op = Name.make ~fixity:Name.Prefix (fst op) in Patt_Data (op, [e]) }
+  | op=PREFIXOP e=prefix_pattern     { let op = Name.make ~fixity:Name.Prefix (fst op) in Patt_Tag (op, [e]) }
 
 simple_pattern: mark_location(plain_simple_pattern) { $1 }
 plain_simple_pattern:
   | UNDERSCORE                     { Patt_Anonymous }
   | x=patt_var                     { Patt_Var x }
-  | x=var_name                     { Patt_Name x } 
+  | x=var_name                     { Patt_Name x }
   | LPAREN p=plain_pattern RPAREN  { p }
+  | LBRACK ps=separated_list(COMMA, pattern) RBRACK { Patt_List ps }
 
 tt_pattern: mark_location(plain_tt_pattern) { $1 }
 plain_tt_pattern:
diff --git a/src/syntax.ml b/src/syntax.ml
index 3b6d3c0a..f856176d 100644
--- a/src/syntax.ml
+++ b/src/syntax.ml
@@ -28,6 +28,8 @@ and pattern' =
   | Patt_Bound of bound
   | Patt_Jdg of tt_pattern * tt_pattern
   | Patt_Tag of Name.ident * pattern list
+  | Patt_Nil
+  | Patt_Cons of pattern * pattern
 
 (** Desugared computations *)
 and comp = comp' * Location.t
@@ -38,6 +40,8 @@ and comp' =
   | Rec of Name.ident * Name.ident * comp
   | Handler of handler
   | Tag of Name.ident * comp list
+  | Nil
+  | Cons of comp * comp
   | Perform of Name.ident * comp list
   | With of comp * comp
   | Let of (Name.ident * comp) list * comp
@@ -148,19 +152,32 @@ let rec shift_tt_pattern k lvl ((p',loc) as p) =
 
 let rec shift_pattern k lvl ((p', loc) as p) =
   match p' with
+
     | Patt_Anonymous -> p
-    | Patt_As (p,k) ->
+
+    | Patt_As (p, k) ->
       let p = shift_pattern k lvl p in
-      Patt_As (p,k), loc
+      Patt_As (p, k), loc
+
     | Patt_Bound m ->
        if m >= lvl then (Patt_Bound (m + k), loc) else p
-    | Patt_Jdg (p1,p2) ->
+
+    | Patt_Jdg (p1, p2) ->
       let p1 = shift_tt_pattern k lvl p1
       and p2 = shift_tt_pattern k lvl p2 in
-      Patt_Jdg (p1,p2), loc
-    | Patt_Tag (t,ps) ->
+      Patt_Jdg (p1, p2), loc
+
+    | Patt_Tag (t, ps) ->
       let ps = List.map (shift_pattern k lvl) ps in
-      Patt_Tag (t,ps), loc
+      Patt_Tag (t, ps), loc
+
+    | Patt_Nil -> Patt_Nil, loc
+
+    | Patt_Cons (p1, p2) ->
+      let p1 = shift_pattern k lvl p1
+      and p2 = shift_pattern k lvl p2 in
+      Patt_Cons (p1, p2), loc
+
 
 let rec shift_comp k lvl (c', loc) =
   let c' =
@@ -176,6 +193,13 @@ let rec shift_comp k lvl (c', loc) =
 
     | Tag (t, lst) -> Tag (t, List.map (shift_comp k lvl) lst)
 
+    | Nil -> Nil
+
+    | Cons (c1, c2) ->
+       let c1 = shift_comp k lvl c1
+       and c2 = shift_comp k lvl c2 in
+       Cons (c1, c2)
+
     | Type -> c'
 
     | Perform (op, cs) ->
diff --git a/src/syntax.mli b/src/syntax.mli
index fbbd7d66..e5f33169 100644
--- a/src/syntax.mli
+++ b/src/syntax.mli
@@ -28,6 +28,8 @@ and pattern' =
   | Patt_Bound of bound
   | Patt_Jdg of tt_pattern * tt_pattern
   | Patt_Tag of Name.ident * pattern list
+  | Patt_Nil
+  | Patt_Cons of pattern * pattern
 
 (** Desugared computations *)
 type comp = comp' * Location.t
@@ -38,6 +40,8 @@ and comp' =
   | Rec of Name.ident * Name.ident * comp
   | Handler of handler
   | Tag of Name.ident * comp list
+  | Nil
+  | Cons of comp * comp
   | Perform of Name.ident * comp list
   | With of comp * comp
   | Let of (Name.ident * comp) list * comp
diff --git a/std/equal.m31 b/std/equal.m31
index bc0be47c..e28645e2 100644
--- a/std/equal.m31
+++ b/std/equal.m31
@@ -39,10 +39,10 @@ matching with e : T gives us a witness of e == e2[??/y]
 (* assoc_update which fails to match if the value to update isn't already present *)
 let assoc_update = fun x v lst =>
   let rec aux acc lst = match lst with
-    | cons (pair x _) ?lst => rev_append acc (cons (pair x v) lst)
-    | cons ?y ?lst => aux (cons y acc) lst
+    | pair x _ :: ?lst => rev_append acc (pair x v :: lst)
+    | ?y :: ?lst => aux (y :: acc) lst
     end
-  in aux nil lst
+  in aux [] lst
 
 (* updates quants with values such that lhs matches rhs *)
 let rec collector quants lhs rhs =
@@ -68,9 +68,9 @@ let rec collector quants lhs rhs =
   end
 
 let rec apply_quants f quants = match quants with
-  | nil => Some f
-  | cons (pair _ None) _ => None
-  | cons (pair _ (Some ?v)) ?quants =>
+  | [] => Some f
+  | pair _ None :: _ => None
+  | pair _ (Some ?v) :: ?quants =>
     apply_quants (f v) quants
   end
 
@@ -88,23 +88,23 @@ let generic_matcher = fun pat e =>
 let process_beta =
   let rec deep quants e b = match b with
     | |- forall (?x : _), ?b =>
-      deep (cons (pair x None) quants) e b
+      deep (pair x None :: quants) e b
     | |- ?lhs == _ => pair e (pair quants lhs)
     end
   in
   fun b => match b with
-    | |- ?e : ?b => deep nil e b
+    | |- ?e : ?b => deep [] e b
     end
 
 let process_hint =
   let rec deep quants e h = match h with
     | |- forall (?x : _), ?h =>
-      deep (cons (pair x None) quants) e h
+      deep (pair x None :: quants) e h
     | |- _ == _ => pair e (pair quants h)
     end
   in
   fun h => match h with
-    | |- ?e : ?h => deep nil e h
+    | |- ?e : ?h => deep [] e h
     end
 
 let sym = λ (A : Type, x y : A, h : x ≡ y), handle refl x : y ≡ x with
@@ -149,8 +149,8 @@ let unopt = fun v => match v with
 (* attempt to apply one of betas to e (not to a subterm of e) *)
 let rec step_at betas e =
   match betas with
-    | nil => None
-    | cons ?b ?rem =>
+    | [] => None
+    | ?b :: ?rem =>
       match generic_matcher b e with
         | (Some _) as ?m => m
         | None => step_at rem e
@@ -260,11 +260,11 @@ let rec equality betas hints = handler
 
   | beta ?b => fun betas hints =>
     let b = process_beta b in
-    yield () (cons b betas) hints
+    yield () (b :: betas) hints
 
   | hint ?h => fun betas hints =>
     let h = process_hint h in
-    yield () betas (cons h hints)
+    yield () betas (h :: hints)
 
   | val ?v => fun betas hints => pair v (pair betas hints)
 
@@ -297,11 +297,11 @@ let equality_in = fun betas hints => handler
 
   | beta ?b => fun betas hints =>
     let b = process_beta b in
-    yield () (cons b betas) hints
+    yield () (b :: betas) hints
 
   | hint ?h => fun betas hints =>
     let h = process_hint h in
-    yield () betas (cons h hints)
+    yield () betas (h :: hints)
 
   | val ?v => fun betas hints => v
 
diff --git a/std/equal_handle.m31 b/std/equal_handle.m31
index c9d982b4..c0df0027 100644
--- a/std/equal_handle.m31
+++ b/std/equal_handle.m31
@@ -1,19 +1,19 @@
 (* equal.m31 should already be included, since we need to set [action] *)
 
 let betas = fun action => match action with
-  | reset => top_betas
+  | reset => !top_betas
   | top_beta ?b =>
-    match (with equality top_betas top_hints handle beta b) with
+    match (with equality !top_betas !top_hints handle beta b) with
       pair _ (pair ?betas _) => betas
     end
-  | top_hint _ => top_betas
+  | top_hint _ => !top_betas
 end
 
-let hints = match top_action with
-  | reset => top_hints
-  | top_beta _ => top_hints
+let hints = match !top_action with
+  | reset => !top_hints
+  | top_beta _ => !top_hints
   | top_hint ?h =>
-    match (with equality top_betas top_hints handle hint h) with
+    match (with equality !top_betas !top_hints handle hint h) with
       pair _ (pair _ ?hints) => hints
     end
 end
diff --git a/std/utils.m31 b/std/utils.m31
index 9c9199cc..10f0043c 100644
--- a/std/utils.m31
+++ b/std/utils.m31
@@ -1,24 +1,23 @@
-
 (** list stuff *)
 let rev =
   let rec rev acc = fun lst => match lst with
-    | nil => acc
-    | cons ?x ?tl => rev (cons x acc) tl
+    | [] => acc
+    | ?x :: ?tl => rev (x :: acc) tl
     end
-  in rev nil
+  in rev []
 
 let rec fold f acc lst = match lst with
-  | nil => acc
-  | cons ?x ?tl => fold (f acc x) tl
+  | [] => acc
+  | ?x :: ?tl => fold (f acc x) tl
   end
 
 let rec assoc_find x lst = match lst with
-  | nil => None
-  | cons (pair x ?v) _ => Some v
-  | cons _ ?lst => assoc_find x lst
+  | [] => None
+  | (pair x ?v) :: _ => Some v
+  | _ :: ?lst => assoc_find x lst
   end
 
-let rev_append = fun l1 l2 => fold (fun acc x => cons x acc) l2 l1
+let rev_append = fun l1 l2 => fold (fun acc x => x :: acc) l2 l1
 
 (** pair stuff *)
 let fst = fun v => match v with
diff --git a/tests/user-equal.m31 b/tests/user-equal.m31
index 8a3b79ae..ffacf8a2 100644
--- a/tests/user-equal.m31
+++ b/tests/user-equal.m31
@@ -1,17 +1,15 @@
-
-
 constant A : Type
 constant a : A
 constant b : A
 constant f : A -> A -> A
 
 
-let test = with equality_in nil nil handle whnf ((lambda x y : A, f y x) a b)
+let test = with equality_in [] [] handle whnf ((lambda x y : A, f y x) a b)
 let _ = print test
 
 constant eq : forall x : A, f a x == b
 
-let action = top_beta eq
+check top_action := !top_beta eq
 
 #include "../std/equal_handle.m31"