Repository: tweag/nickel
Pull request #234 (2020-12-02 12:18:02)

[Refactor]Remove the previous representation of metavalues
Depend on #233. Cleanup of dead code following #233.


Patch:
diff --git a/src/error.rs b/src/error.rs
index def5520d..6fcc74cf 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -87,12 +87,6 @@ pub enum TypecheckError {
         /* the inferred/annotated type */ Types,
         Option<RawSpan>,
     ),
-    /// A dynamic tail was expected to be in the type of an expression, but was not.
-    MissingDynTail(
-        /* the expected type */ Types,
-        /* the inferred/annotated type */ Types,
-        Option<RawSpan>,
-    ),
     /// A specific row was not expected to be in the type of an expression.
     ExtraRow(
         Ident,
@@ -100,13 +94,6 @@ pub enum TypecheckError {
         /* the inferred/annotated type */ Types,
         Option<RawSpan>,
     ),
-    /// A additional dynamic tail was not expected to be in the type of an expression.
-    ExtraDynTail(
-        /* the expected type */ Types,
-        /* the inferred/annotated type */ Types,
-        Option<RawSpan>,
-    ),
-
     /// An unbound type variable was referenced.
     UnboundTypeVariable(Ident, Option<RawSpan>),
     /// The actual (inferred or annotated) type of an expression is incompatible with its expected
@@ -969,16 +956,6 @@ impl ToDiagnostic<FileId> for TypecheckError {
                         format!("The type of the expression was inferred to be `{}`, which does not contain the field `{}`", actual,  ident),
                     ])]
             ,
-            TypecheckError::MissingDynTail(expd, actual, span_opt) =>
-                vec![Diagnostic::error()
-                    .with_message(String::from("Type error: missing dynamic tail `| Dyn`"))
-                    .with_labels(mk_expr_label(span_opt))
-                    .with_notes(vec![
-                        format!("The type of the expression was expected to be `{}` which contains the tail `| Dyn`", expd),
-                        format!("The type of the expression was inferred to be `{}`, which does not contain the tail `| Dyn`", actual),
-                    ])]
-            ,
-
             TypecheckError::ExtraRow(Ident(ident), expd, actual, span_opt) =>
                 vec![Diagnostic::error()
                     .with_message(format!("Type error: extra row `{}`", ident))
@@ -988,16 +965,6 @@ impl ToDiagnostic<FileId> for TypecheckError {
                         format!("Tye type of the expression was inferred to be `{}`, which contains the extra field `{}`", actual,  ident),
                     ])]
             ,
-            TypecheckError::ExtraDynTail(expd, actual, span_opt) =>
-                vec![Diagnostic::error()
-                    .with_message(String::from("Type error: extra dynamic tail `| Dyn`"))
-                    .with_labels(mk_expr_label(span_opt))
-                    .with_notes(vec![
-                        format!("The type of the expression was expected to be `{}`, which does not contain the tail `| Dyn`", expd),
-                        format!("Tye type of the expression was inferred to be `{}`, which contains the extra tail `| Dyn`", actual),
-                    ])]
-            ,
-
             TypecheckError::UnboundTypeVariable(Ident(ident), span_opt) =>
                vec![Diagnostic::error()
                     .with_message(String::from("Unbound type variable"))
diff --git a/src/eval.rs b/src/eval.rs
index 8d6a0576..70c0bc6b 100644
--- a/src/eval.rs
+++ b/src/eval.rs
@@ -429,51 +429,6 @@ where
                     return Err(EvalError::Other(String::from("empty metavalue"), pos));
                 }
             }
-            Term::Contract(_, _) if enriched_strict => {
-                return Err(EvalError::Other(
-                    String::from(
-                        "Expected a simple term, got a Contract. Contracts cannot be evaluated",
-                    ),
-                    pos,
-                ));
-            }
-            enriched @ Term::DefaultValue(_) | enriched @ Term::Docstring(_, _)
-                if enriched_strict =>
-            {
-                /* Since we are forcing an enriched value, we are morally breaking subject
-                 * reduction (i.e., the type of the current term changes from `enriched something`
-                 * to just `something`). Updating a thunk after having performed this forcing may
-                 * alter the semantics of the program in an unexpected way (see issue
-                 * https://github.com/tweag/nickel/issues/123): we update potential thunks now so
-                 * that their content remains an enriched value.
-                 */
-                let update_closure = Closure {
-                    body: RichTerm {
-                        term: Box::new(enriched),
-                        pos,
-                    },
-                    env,
-                };
-                update_thunks(&mut stack, &update_closure);
-
-                let Closure {
-                    body:
-                        RichTerm {
-                            term: enriched_box,
-                            pos: _,
-                        },
-                    env,
-                } = update_closure;
-                let t = match *enriched_box {
-                    Term::DefaultValue(t) | Term::Docstring(_, t) => t,
-                    _ => panic!("eval::eval(): previous match enforced that a term is a default or a docstring, but matched something else")
-                };
-                Closure { body: t, env }
-            }
-            Term::ContractWithDefault(ty, label, t) if enriched_strict => Closure {
-                body: Term::Assume(ty, label, t).into(),
-                env,
-            },
             Term::ResolvedImport(id) => {
                 if let Some(t) = resolver.get(id) {
                     Closure::atomic_closure(t)
@@ -685,35 +640,6 @@ fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichTerm
 
                 RichTerm::new(Term::StrChunks(chunks), pos)
             }
-            Term::Contract(ty, label) => {
-                let ty = match ty {
-                    Types(AbsType::Flat(t)) => {
-                        Types(AbsType::Flat(subst_(t, global_env, env, bound)))
-                    }
-                    ty => ty,
-                };
-
-                RichTerm::new(Term::Contract(ty, label), pos)
-            }
-            Term::DefaultValue(t) => {
-                let t = subst_(t, global_env, env, bound);
-
-                RichTerm::new(Term::DefaultValue(t), pos)
-            }
-            Term::ContractWithDefault(ty, lbl, t) => {
-                let ty = match ty {
-                    Types(AbsType::Flat(t)) => Types(AbsType::Flat(subst_(
-                        t,
-                        global_env,
-                        env,
-                        Cow::Borrowed(bound.as_ref()),
-                    ))),
-                    ty => ty,
-                };
-                let t = subst_(t, global_env, env, bound);
-
-                RichTerm::new(Term::ContractWithDefault(ty, lbl, t), pos)
-            }
             Term::MetaValue(meta) => {
                 let contract = meta.contract.map(|(ty, lbl)| {
                     let ty = match ty {
@@ -740,11 +666,6 @@ fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichTerm
 
                 RichTerm::new(Term::MetaValue(meta), pos)
             }
-            Term::Docstring(s, t) => {
-                let t = subst_(t, global_env, env, bound);
-
-                RichTerm::new(Term::Docstring(s, t), pos)
-            }
         }
     }
 
@@ -842,6 +763,12 @@ mod tests {
         assert_eq!(Ok(Term::Num(12.5)), eval_no_import(t));
     }
 
+    #[test]
+    fn simple_is_zero() {
+        let t = mk_term::op1(UnaryOp::IsZero(), Term::Num(7.0));
+        assert_eq!(Ok(Term::Bool(false)), eval_no_import(t));
+    }
+
     #[test]
     fn asking_for_various_types() {
         let num = mk_term::op1(UnaryOp::IsNum(), Term::Num(45.3));
@@ -857,13 +784,27 @@ mod tests {
         assert_eq!(Ok(Term::Bool(true)), eval_no_import(lambda));
     }
 
+    fn mk_default(t: RichTerm) -> Term {
+        use crate::term::MergePriority;
+
+        let mut meta = MetaValue::from(t);
+        meta.priority = MergePriority::Default;
+        Term::MetaValue(meta)
+    }
+
+    fn mk_docstring<S>(t: RichTerm, s: S) -> Term
+    where
+        S: Into<String>,
+    {
+        let mut meta = MetaValue::from(t);
+        meta.doc.replace(s.into());
+        Term::MetaValue(meta)
+    }
+
     #[test]
     fn enriched_terms_unwrapping() {
-        let t = Term::DefaultValue(
-            Term::DefaultValue(Term::Docstring("a".to_string(), Term::Bool(false).into()).into())
-                .into(),
-        )
-        .into();
+        let t = mk_default(mk_default(mk_docstring(Term::Bool(false).into(), "a").into()).into())
+            .into();
         assert_eq!(Ok(Term::Bool(false)), eval_no_import(t));
     }
 
@@ -872,7 +813,7 @@ mod tests {
         let t = mk_term::op2(
             BinaryOp::Merge(),
             Term::Num(1.0),
-            Term::DefaultValue(Term::Num(2.0).into()),
+            mk_default(Term::Num(2.0).into()),
         );
         assert_eq!(Ok(Term::Num(1.0)), eval_no_import(t));
     }
@@ -881,8 +822,8 @@ mod tests {
     fn merge_incompatible_defaults() {
         let t = mk_term::op2(
             BinaryOp::Merge(),
-            Term::DefaultValue(Term::Num(1.0).into()),
-            Term::DefaultValue(Term::Num(2.0).into()),
+            mk_default(Term::Num(1.0).into()),
+            mk_default(Term::Num(2.0).into()),
         );
 
         eval_no_import(t).unwrap_err();
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 050dab18..8dfdd274 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -271,6 +271,7 @@ ChunkLiteralPart: Either<&'input str, char> = {
     };
 
 UOp: UnaryOp<RichTerm> = {
+    "isZero" => UnaryOp::IsZero(),
     "isNum" => UnaryOp::IsNum(),
     "isBool" => UnaryOp::IsBool(),
     "isStr" => UnaryOp::IsStr(),
@@ -290,8 +291,7 @@ UOp: UnaryOp<RichTerm> = {
             ds.into_iter().map(|x| x.0).collect(),
             default,
         ),
-    "map" <Atom> => UnaryOp::ListMap(<>),
-    "recordMap" <Atom> => UnaryOp::RecordMap(<>),
+    "mapRec" <Atom> => UnaryOp::MapRec(<>),
     "seq" => UnaryOp::Seq(),
     "deepSeq" => UnaryOp::DeepSeq(),
     "head" => UnaryOp::ListHead(),
@@ -414,6 +414,7 @@ BOpPre: BinaryOp<RichTerm> = {
     "unwrap" => BinaryOp::Unwrap(),
     "goField" => BinaryOp::GoField(),
     "hasField" => BinaryOp::HasField(),
+    "map" => BinaryOp::ListMap(),
     "elemAt" => BinaryOp::ListElemAt(),
 }
 
@@ -439,11 +440,6 @@ BaseType: Types = {
     "List" => Types(AbsType::List()),
 };
 
-RowTail: Types = {
-    <Ident> => Types(AbsType::Var(<>)),
-    "Dyn" => Types(AbsType::Dyn()),
-}
-
 subType : Types = {
     <BaseType>,
     <Ident> => Types(AbsType::Var(<>)),
@@ -470,7 +466,7 @@ subType : Types = {
     },
     "{" <rows:(<Ident> ":" <Types> ",")*>
         <last:(<Ident> ":" <Types>)?>
-        <tail: ("|" <RowTail>)?> "}" => {
+        <tail: ("|" <Ident>)?> "}" => {
         let ty = rows.into_iter()
             .chain(last.into_iter())
             // As we build row types as a linked list via a fold on the original
@@ -479,7 +475,12 @@ subType : Types = {
             // order for error reporting.
             .rev()
             .fold(
-                tail.unwrap_or(Types(AbsType::RowEmpty())),
+                Types(
+                    match tail {
+                        Some(id) => AbsType::Var(id),
+                        None => AbsType::RowEmpty(),
+                    }
+                ),
                 |t, i_ty| {
                     let (i, ty) = i_ty;
                     Types(AbsType::RowExtend(i, Some(Box::new(ty)), Box::new(t)))
@@ -567,6 +568,7 @@ extern {
         "ContractDefault(" => Token::Normal(NormalToken::ContractDeflt),
         "Docstring(" => Token::Normal(NormalToken::Docstring),
 
+        "isZero" => Token::Normal(NormalToken::IsZero),
         "isNum" => Token::Normal(NormalToken::IsNum),
         "isBool" => Token::Normal(NormalToken::IsBool),
         "isStr" => Token::Normal(NormalToken::IsStr),
@@ -582,7 +584,7 @@ extern {
         "wrap" => Token::Normal(NormalToken::Wrap),
         "unwrap" => Token::Normal(NormalToken::Unwrap),
         "embed" => Token::Normal(NormalToken::Embed),
-        "recordMap" => Token::Normal(NormalToken::RecordMap),
+        "mapRec" => Token::Normal(NormalToken::MapRec),
         "seq" => Token::Normal(NormalToken::Seq),
         "deepSeq" => Token::Normal(NormalToken::DeepSeq),
         "head" => Token::Normal(NormalToken::Head),
@@ -593,6 +595,7 @@ extern {
         "hasField" => Token::Normal(NormalToken::HasField),
         "map" => Token::Normal(NormalToken::Map),
         "elemAt" => Token::Normal(NormalToken::ElemAt),
+        "merge" => Token::Normal(NormalToken::Merge),
 
         "{" => Token::Normal(NormalToken::LBrace),
         "}" => Token::Normal(NormalToken::RBrace),
diff --git a/src/merge.rs b/src/merge.rs
index f82d04a0..c2bba3a0 100644
--- a/src/merge.rs
+++ b/src/merge.rs
@@ -11,7 +11,7 @@
 //! - All the fields of `r1` that are not in `r2`
 //! - All the fields of `r2` that are not in `r1`
 //! - Fields that are both in `r1` and `r2` are recursively merged: for a field `f`, the result
-//! contains the binding `f = r1.f & r2.f`
+//! contains the binding `f = merge r1.f r2.f`
 //!
 //! As fields are recursively merged, merge needs to operate on any value, not only on records.
 //!
@@ -246,138 +246,6 @@ pub fn merge(
                 env,
             })
         }
-        // Right-biased: when merging two docstrings (s1,t2) and (s2,t2), the right one will end up
-        // as the outermost position in the resulting term (s2,(s1,merge t1 t2))
-        (t1, Term::Docstring(s, t2)) => {
-            let Closure { body, env } = mk_merge_closure(
-                RichTerm {
-                    term: Box::new(t1),
-                    pos: pos1,
-                },
-                env1,
-                t2,
-                env2,
-            );
-            let body = Term::Docstring(s, body).into();
-            Ok(Closure { body, env })
-        }
-        (Term::Docstring(s, t1), t2) => {
-            let Closure { body, env } = mk_merge_closure(
-                t1,
-                env1,
-                RichTerm {
-                    term: Box::new(t2),
-                    pos: pos2,
-                },
-                env2,
-            );
-            let body = Term::Docstring(s, body).into();
-            Ok(Closure { body, env })
-        }
-        // Default merging
-        (Term::DefaultValue(t1), Term::DefaultValue(t2)) => {
-            let Closure { body, env } = mk_merge_closure(t1, env1, t2, env2);
-            let body = Term::DefaultValue(body).into();
-            Ok(Closure { body, env })
-        }
-        (Term::DefaultValue(t1), Term::ContractWithDefault(ty, lbl, t2))
-        | (Term::ContractWithDefault(ty, lbl, t2), Term::DefaultValue(t1)) => {
-            let Closure { body, mut env } = mk_merge_closure(t1, env1, t2, env2.clone());
-            let ty_closure = ty.closurize(&mut env, env2);
-            let body = Term::ContractWithDefault(ty_closure, lbl, body).into();
-            Ok(Closure { body, env })
-        }
-        // Composed contracts carry and blame their original label. As any contract, the composite
-        // still requires a label, but it will be ignored, so we can provide a dummy one.
-        (Term::ContractWithDefault(ty1, lbl1, t1), Term::ContractWithDefault(ty2, lbl2, t2)) => {
-            let Closure { body, mut env } = mk_merge_closure(t1, env1.clone(), t2, env2.clone());
-            let body = Term::ContractWithDefault(
-                merge_types_closure(&mut env, ty1, lbl1, env1, ty2, lbl2, env2),
-                Label::dummy(),
-                body,
-            )
-            .into();
-            Ok(Closure { body, env })
-        }
-        // We need to keep the environment of contracts as well: custom contracts may use variables
-        // from the environment, and even standard contracts need access to builtins contracts (see
-        // issue https://github.com/tweag/nickel/issues/117)
-        (Term::DefaultValue(t), Term::Contract(ty, lbl)) => {
-            let mut env = HashMap::new();
-            let t_closure = t.closurize(&mut env, env1);
-            let ty_closure = ty.closurize(&mut env, env2);
-            let body = Term::ContractWithDefault(ty_closure, lbl, t_closure).into();
-            Ok(Closure { body, env })
-        }
-        (Term::Contract(ty, lbl), Term::DefaultValue(t)) => {
-            let mut env = HashMap::new();
-            let ty_closure = ty.closurize(&mut env, env1);
-            let t_closure = t.closurize(&mut env, env2);
-            let body = Term::ContractWithDefault(ty_closure, lbl, t_closure).into();
-            Ok(Closure { body, env })
-        }
-        (Term::DefaultValue(_), t) => {
-            let body = RichTerm {
-                term: Box::new(t),
-                pos: pos2,
-            };
-            Ok(Closure { body, env: env2 })
-        }
-        (t, Term::DefaultValue(_)) => {
-            let body = RichTerm {
-                term: Box::new(t),
-                pos: pos1,
-            };
-            Ok(Closure { body, env: env1 })
-        }
-        // Contracts merging
-        (Term::Contract(ty1, lbl1), Term::Contract(ty2, lbl2)) => {
-            let mut env = HashMap::new();
-            let body = Term::Contract(
-                merge_types_closure(&mut env, ty1, lbl1, env1, ty2, lbl2, env2),
-                Label::dummy(),
-            )
-            .into();
-            Ok(Closure { body, env })
-        }
-        (Term::Contract(ty1, lbl1), Term::ContractWithDefault(ty2, lbl2, t)) => {
-            let mut env = HashMap::new();
-            let ty_closure =
-                merge_types_closure(&mut env, ty1, lbl1, env1, ty2, lbl2, env2.clone());
-            let t_closure = t.closurize(&mut env, env2);
-            let body = Term::ContractWithDefault(ty_closure, Label::dummy(), t_closure).into();
-            Ok(Closure { body, env })
-        }
-        (Term::ContractWithDefault(ty1, lbl1, t), Term::Contract(ty2, lbl2)) => {
-            let mut env = HashMap::new();
-            let ty_closure =
-                merge_types_closure(&mut env, ty1, lbl1, env1.clone(), ty2, lbl2, env2);
-            let t_closure = t.closurize(&mut env, env1);
-            let body = Term::ContractWithDefault(ty_closure, Label::dummy(), t_closure).into();
-            Ok(Closure { body, env })
-        }
-        (Term::Contract(ty, lbl), t) | (Term::ContractWithDefault(ty, lbl, _), t) => {
-            let mut env = HashMap::new();
-            let t = RichTerm {
-                term: Box::new(t),
-                pos: pos2,
-            };
-            let ty_closure = ty.closurize(&mut env, env1);
-            let t_closure = t.closurize(&mut env, env2);
-            let body = Term::Assume(ty_closure, lbl, t_closure).into();
-            Ok(Closure { body, env })
-        }
-        (t, Term::Contract(ty, lbl)) | (t, Term::ContractWithDefault(ty, lbl, _)) => {
-            let mut env = HashMap::new();
-            let t = RichTerm {
-                term: Box::new(t),
-                pos: pos1,
-            };
-            let t_closure = t.closurize(&mut env, env1);
-            let ty_closure = ty.closurize(&mut env, env2);
-            let body = Term::Assume(ty_closure, lbl, t_closure).into();
-            Ok(Closure { body, env })
-        }
         // Merge put together the fields of records, and recursively merge
         // fields that are present in both terms
         (Term::Record(m1), Term::Record(m2)) => {
@@ -469,15 +337,6 @@ fn merge_closurize(
     body.closurize(env, local_env)
 }
 
-/// Take two terms together with their environment, and return a closure representing their merge.
-/// Just call [`merge_closurize`](./fn.merge_closurize.html) in a new environment and return the
-/// result.
-fn mk_merge_closure(t1: RichTerm, env1: Environment, t2: RichTerm, env2: Environment) -> Closure {
-    let mut env = HashMap::new();
-    let body = merge_closurize(&mut env, t1, env1, t2, env2);
-    Closure { body, env }
-}
-
 /// Compose two contracts, given as terms.
 ///
 /// To compose contracts `c1` and `c2`, construct the term `fun _l x => c1 l1 (c2 l2 x)`, where
diff --git a/src/operation.rs b/src/operation.rs
index 698ca7fa..08db7e43 100644
--- a/src/operation.rs
+++ b/src/operation.rs
@@ -15,31 +15,16 @@ use crate::merge;
 use crate::merge::merge;
 use crate::position::RawSpan;
 use crate::stack::Stack;
+use crate::stdlib;
 use crate::term::make as mk_term;
 use crate::term::{BinaryOp, RichTerm, StrChunk, Term, UnaryOp};
 use crate::transformations::Closurizable;
 use crate::{mk_app, mk_fun};
 use simple_counter::*;
 use std::collections::HashMap;
-use std::iter::Extend;
 
 generate_counter!(FreshVariableCounter, usize);
 
-/// Result of the equality of two terms.
-///
-/// The equality of two terms can either be computed directly for base types (`Num`, `Str`, etc.),
-/// in which case `Bool` is returned. Otherwise, composite values such as lists or records generate
-/// new subequalities, as represented by the last variant as a vector of pairs of terms.  This list
-/// should be non-empty (it if was empty, `eq` should have returned `Bool(true)` directly).  The
-/// first element of this non-empty list is encoded as the two first parameters of `Eqs`, while the
-/// last vector parameter is the (potentially empty) tail.
-///
-/// See [`eq`](./fn.eq.html).
-enum EqResult {
-    Bool(bool),
-    Eqs(RichTerm, RichTerm, Vec<(Closure, Closure)>),
-}
-
 /// An operation continuation as stored on the stack.
 #[derive(Debug, PartialEq)]
 pub enum OperationCont {
@@ -139,6 +124,19 @@ fn process_unary_operation(
                 ))
             }
         }
+        UnaryOp::IsZero() => {
+            if let Term::Num(n) = *t {
+                // TODO Discuss and decide on this comparison for 0 on f64
+                Ok(Closure::atomic_closure(Term::Bool(n == 0.).into()))
+            } else {
+                Err(EvalError::TypeError(
+                    String::from("Num"),
+                    String::from("isZero"),
+                    arg_pos,
+                    RichTerm { term: t, pos },
+                ))
+            }
+        }
         UnaryOp::IsNum() => {
             if let Term::Num(_) = *t {
                 Ok(Closure::atomic_closure(Term::Bool(true).into()))
@@ -407,57 +405,24 @@ fn process_unary_operation(
                 ))
             }
         }
-        UnaryOp::ListMap(f) => {
-            if let Term::List(ts) = *t {
-                let mut shared_env = Environment::new();
-                let f_as_var = f.body.closurize(&mut env, f.env);
-
-                // List elements are closurized to preserve lazyness of data structures. It
-                // maintains the invariant that any data structure only contain thunks (that is,
-                // currently, variables).
-                let ts = ts
-                    .into_iter()
-                    .map(|t| {
-                        RichTerm::from(Term::App(f_as_var.clone(), t))
-                            .closurize(&mut shared_env, env.clone())
-                            .into()
-                    })
-                    .collect();
-
-                Ok(Closure {
-                    body: Term::List(ts).into(),
-                    env: shared_env,
-                })
-            } else {
-                Err(EvalError::TypeError(
-                    String::from("List"),
-                    String::from("map, 2nd argument"),
-                    arg_pos,
-                    RichTerm { term: t, pos },
-                ))
-            }
-        }
-        UnaryOp::RecordMap(f) => {
+        UnaryOp::MapRec(f) => {
             if let Term::Record(rec) = *t {
-                let mut shared_env = Environment::new();
                 let f_as_var = f.body.closurize(&mut env, f.env);
 
-                // As for `ListMap` (see above), we closurize the content of fields
                 let rec = rec
                     .into_iter()
                     .map(|e| {
                         let (Ident(s), t) = e;
                         (
                             Ident(s.clone()),
-                            mk_app!(f_as_var.clone(), mk_term::string(s), t)
-                                .closurize(&mut shared_env, env.clone()),
+                            mk_app!(f_as_var.clone(), mk_term::string(s), t.clone()),
                         )
                     })
                     .collect();
 
                 Ok(Closure {
                     body: Term::Record(rec).into(),
-                    env: shared_env,
+                    env,
                 })
             } else {
                 Err(EvalError::TypeError(
@@ -638,7 +603,7 @@ fn process_binary_operation(
     fst_pos: Option<RawSpan>,
     clos: Closure,
     snd_pos: Option<RawSpan>,
-    stack: &mut Stack,
+    _stack: &mut Stack,
     pos_op: Option<RawSpan>,
 ) -> Result<Closure, EvalError> {
     let Closure {
@@ -853,49 +818,64 @@ fn process_binary_operation(
             }
         }
         BinaryOp::Eq() => {
-            let mut env = Environment::new();
-
-            let c1 = Closure {
-                body: RichTerm {
-                    term: t1,
-                    pos: pos1,
-                },
-                env: env1,
-            };
-            let c2 = Closure {
-                body: RichTerm {
-                    term: t2,
-                    pos: pos2,
-                },
-                env: env2,
-            };
+            /// Take an iterator of pairs of RichTerm, the common environments of all left
+            /// components of these pairs and all right components, the final environment,
+            /// and build a Term which evaluates to `Bool(true)` if and only if all the pairs are
+            /// equals
+            fn eq_all<T>(
+                it: T,
+                env1: &Environment,
+                env2: &Environment,
+                env: &mut Environment,
+            ) -> Term
+            where
+                T: Iterator<Item = (RichTerm, RichTerm)>,
+            {
+                let subeqs: Vec<RichTerm> = it
+                    .map(|(t1, t2)| {
+                        let t1_var = t1.closurize(env, env1.clone());
+                        let t2_var = t2.closurize(env, env2.clone());
+                        Term::Op2(BinaryOp::Eq(), t1_var, t2_var).into()
+                    })
+                    .collect();
+                // lists.all (fun x => x) subeqs
+                Term::App(
+                    mk_app!(stdlib::lists::all(), mk_term::id()),
+                    Term::List(subeqs).into(),
+                )
+            }
 
-            match eq(&mut env, c1, c2) {
-                EqResult::Bool(b) => match (b, stack.pop_eq()) {
-                    (false, _) => {
-                        stack.clear_eqs();
-                        Ok(Closure::atomic_closure(Term::Bool(false).into()))
-                    }
-                    (true, None) => Ok(Closure::atomic_closure(Term::Bool(true).into())),
-                    (true, Some((c1, c2))) => {
-                        let t1 = c1.body.closurize(&mut env, c1.env);
-                        let t2 = c2.body.closurize(&mut env, c2.env);
+            let mut env: Environment = HashMap::new();
+            let res = match (*t1, *t2) {
+                (Term::Bool(b1), Term::Bool(b2)) => Term::Bool(b1 == b2),
+                (Term::Num(n1), Term::Num(n2)) => Term::Bool(n1 == n2),
+                (Term::Str(s1), Term::Str(s2)) => Term::Bool(s1 == s2),
+                (Term::Lbl(l1), Term::Lbl(l2)) => Term::Bool(l1 == l2),
+                (Term::Sym(s1), Term::Sym(s2)) => Term::Bool(s1 == s2),
+                (Term::Record(m1), Term::Record(m2)) => {
+                    let (left, center, right) = merge::hashmap::split(m1, m2);
 
-                        Ok(Closure {
-                            body: RichTerm::new(Term::Op2(BinaryOp::Eq(), t1, t2), pos_op),
-                            env,
-                        })
+                    if !left.is_empty() || !right.is_empty() {
+                        Term::Bool(false)
+                    } else {
+                        eq_all(
+                            center.into_iter().map(|(_, (t1, t2))| (t1, t2)),
+                            &env1,
+                            &env2,
+                            &mut env,
+                        )
                     }
-                },
-                EqResult::Eqs(t1, t2, subeqs) => {
-                    stack.push_eqs(subeqs.into_iter());
-
-                    Ok(Closure {
-                        body: RichTerm::new(Term::Op2(BinaryOp::Eq(), t1, t2), pos_op),
-                        env,
-                    })
                 }
-            }
+                (Term::List(l1), Term::List(l2)) if l1.len() == l2.len() => {
+                    eq_all(l1.into_iter().zip(l2.into_iter()), &env1, &env2, &mut env)
+                }
+                (_, _) => Term::Bool(false),
+            };
+
+            Ok(Closure {
+                body: res.into(),
+                env,
+            })
         }
         BinaryOp::LessThan() => {
             if let Term::Num(n1) = *t1 {
@@ -1208,6 +1188,36 @@ fn process_binary_operation(
                 },
             )),
         },
+        // This one should not be strict in the first argument (f)
+        BinaryOp::ListMap() => {
+            if let Term::List(ts) = *t2 {
+                let f = RichTerm {
+                    term: t1,
+                    pos: pos1,
+                };
+                let f_as_var = f.closurize(&mut env2, env1);
+
+                let ts = ts
+                    .into_iter()
+                    .map(|t| Term::App(f_as_var.clone(), t).into())
+                    .collect();
+
+                Ok(Closure {
+                    body: Term::List(ts).into(),
+                    env: env2,
+                })
+            } else {
+                Err(EvalError::TypeError(
+                    String::from("List"),
+                    String::from("map, 2nd argument"),
+                    snd_pos,
+                    RichTerm {
+                        term: t2,
+                        pos: pos2,
+                    },
+                ))
+            }
+        }
         BinaryOp::ListElemAt() => match (*t1, *t2) {
             (Term::List(mut ts), Term::Num(n)) => {
                 let n_int = n as usize;
@@ -1257,89 +1267,6 @@ fn process_binary_operation(
     }
 }
 
-/// Compute the equality of two terms, represented as closures.
-///
-/// # Parameters
-///
-/// - env: the final environment in which to closurize the operands of potential subequalities.
-/// - c1: the closure of the first operand.
-/// - c2: the closure of the second operand.
-///
-/// # Return
-///
-/// Return either a boolean when the equality can be computed directly, or a new non-empty list of equalities to be checked if
-/// operands are composite values.
-fn eq(env: &mut Environment, c1: Closure, c2: Closure) -> EqResult {
-    let Closure {
-        body: RichTerm { term: t1, .. },
-        env: env1,
-    } = c1;
-    let Closure {
-        body: RichTerm { term: t2, .. },
-        env: env2,
-    } = c2;
-
-    // Take a list of subequalities, and either return `EqResult::Bool(true)` if it is empty, or
-    // generate an approriate `EqResult::Eqs` variant with closurized terms in it.
-    fn gen_eqs<I>(
-        mut it: I,
-        env: &mut Environment,
-        env1: Environment,
-        env2: Environment,
-    ) -> EqResult
-    where
-        I: Iterator<Item = (RichTerm, RichTerm)>,
-    {
-        if let Some((t1, t2)) = it.next() {
-            let eqs = it
-                .map(|(t1, t2)| {
-                    (
-                        Closure {
-                            body: t1,
-                            env: env1.clone(),
-                        },
-                        Closure {
-                            body: t2,
-                            env: env2.clone(),
-                        },
-                    )
-                })
-                .collect();
-
-            EqResult::Eqs(t1.closurize(env, env1), t2.closurize(env, env2), eqs)
-        } else {
-            EqResult::Bool(true)
-        }
-    }
-
-    match (*t1, *t2) {
-        (Term::Bool(b1), Term::Bool(b2)) => EqResult::Bool(b1 == b2),
-        (Term::Num(n1), Term::Num(n2)) => EqResult::Bool(n1 == n2),
-        (Term::Str(s1), Term::Str(s2)) => EqResult::Bool(s1 == s2),
-        (Term::Lbl(l1), Term::Lbl(l2)) => EqResult::Bool(l1 == l2),
-        (Term::Sym(s1), Term::Sym(s2)) => EqResult::Bool(s1 == s2),
-        (Term::Record(m1), Term::Record(m2)) => {
-            let (left, center, right) = merge::hashmap::split(m1, m2);
-
-            if !left.is_empty() || !right.is_empty() {
-                EqResult::Bool(false)
-            } else if center.is_empty() {
-                EqResult::Bool(true)
-            } else {
-                let eqs = center.into_iter().map(|(_, (t1, t2))| (t1, t2));
-                gen_eqs(eqs.into_iter(), env, env1, env2)
-            }
-        }
-        (Term::List(l1), Term::List(l2)) if l1.len() == l2.len() => {
-            // Equalities are tested in reverse order, but that shouldn't matter. If it
-            // does, just do `eqs.rev()`
-            let eqs = l1.into_iter().zip(l2.into_iter());
-            gen_eqs(eqs.into_iter(), env, env1, env2)
-        }
-        (_, _) => EqResult::Bool(false),
-    }
-}
-
 #[cfg(test)]
 mod tests {
     use super::*;
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index c08a820d..ca098a79 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -141,7 +141,7 @@ pub enum NormalToken<'input> {
     #[regex("m(#+)\"", |lex| lex.slice().len())]
     MultiStringStart(usize),
 
-    #[token("%tag%")]
+    #[token("tag")]
     Tag,
     #[token("Assume(")]
     Assume,
@@ -156,59 +156,63 @@ pub enum NormalToken<'input> {
     #[token("Docstring(")]
     Docstring,
 
-    #[token("%isNum%")]
+    #[token("isZero")]
+    IsZero,
+    #[token("isNum")]
     IsNum,
-    #[token("%isBool%")]
+    #[token("isBool")]
     IsBool,
-    #[token("%isStr%")]
+    #[token("isStr")]
     IsStr,
-    #[token("%isFun%")]
+    #[token("isFun")]
     IsFun,
-    #[token("%isList%")]
+    #[token("isList")]
     IsList,
-    #[token("%isRecord%")]
+    #[token("isRecord")]
     IsRecord,
 
-    #[token("%blame%")]
+    #[token("blame")]
     Blame,
-    #[token("%chngPol%")]
+    #[token("chngPol")]
     ChangePol,
-    #[token("%polarity%")]
+    #[token("polarity")]
     Polarity,
-    #[token("%goDom%")]
+    #[token("goDom")]
     GoDom,
-    #[token("%goCodom%")]
+    #[token("goCodom")]
     GoCodom,
-    #[token("%goField%")]
+    #[token("goField")]
     GoField,
 
-    #[token("%wrap%")]
+    #[token("wrap")]
     Wrap,
-    #[token("%unwrap%")]
-    Unwrap,
-    #[token("%embed%")]
+    #[token("embed")]
     Embed,
-    #[token("%recordMap%")]
-    RecordMap,
-    #[token("%seq%")]
+    #[token("mapRec")]
+    MapRec,
+    #[token("seq")]
     Seq,
-    #[token("%deepSeq%")]
+    #[token("deepSeq")]
     DeepSeq,
-    #[token("%head%")]
+    #[token("head")]
     Head,
-    #[token("%tail%")]
+    #[token("tail")]
     Tail,
-    #[token("%length%")]
+    #[token("length")]
     Length,
-    #[token("%fieldsOf%")]
+    #[token("fieldsOf")]
     FieldsOf,
 
-    #[token("%hasField%")]
+    #[token("unwrap")]
+    Unwrap,
+    #[token("hasField")]
     HasField,
-    #[token("%map%")]
+    #[token("map")]
     Map,
-    #[token("%elemAt%")]
+    #[token("elemAt")]
     ElemAt,
+    #[token("merge")]
+    Merge,
 
     #[token("{")]
     LBrace,
@@ -230,8 +234,6 @@ pub enum NormalToken<'input> {
     RAngleBracket,
     #[token(">=")]
     GreaterOrEq,
-    #[regex("//[^\n]*")]
-    LineComment,
 }
 
 /// The tokens in string mode.
@@ -540,8 +542,6 @@ impl<'input> Iterator for Lexer<'input> {
             | Some(MultiStr(MultiStringToken::Error)) => {
                 return Some(Err(LexicalError::Generic(span.start, span.end)))
             }
-            // Ignore comment
-            Some(Normal(NormalToken::LineComment)) => return self.next(),
             _ => (),
         }
 
diff --git a/src/program.rs b/src/program.rs
index 836c0c09..af9d948a 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -181,22 +181,12 @@ impl Program {
     fn mk_global_env(&mut self) -> Result<eval::Environment, ImportError> {
         let mut global_env = HashMap::new();
 
-        self.load_stdlib(
-            "<stdlib/builtins.ncl>",
-            nickel_stdlib::BUILTINS,
-            &mut global_env,
-        )?;
         self.load_stdlib(
             "<stdlib/contracts.ncl>",
             nickel_stdlib::CONTRACTS,
             &mut global_env,
         )?;
         self.load_stdlib("<stdlib/lists.ncl>", nickel_stdlib::LISTS, &mut global_env)?;
-        self.load_stdlib(
-            "<stdlib/records.ncl>",
-            nickel_stdlib::RECORDS,
-            &mut global_env,
-        )?;
         Ok(global_env)
     }
 
@@ -590,7 +580,7 @@ mod tests {
 
     #[test]
     fn simple_type_check() {
-        let res = eval_string("let x = 5 in if %isNum% x then true else 1");
+        let res = eval_string("let x = 5 in if isNum x then true else 1");
 
         assert_eq!(Ok(Term::Bool(true)), res);
     }
@@ -624,7 +614,7 @@ g true",
             let or : Bool -> Bool -> Bool = fun x => fun y => if x then x else y in
 
             let fibo : Num -> Num = Y (fun fibo =>
-                (fun x => if or (x == 0) (dec x == 0) then 1 else (fibo (dec x)) + (fibo (dec (dec x))))) in
+                (fun x => if or (isZero x) (isZero (dec x)) then 1 else (fibo (dec x)) + (fibo (dec (dec x))))) in
             let val : Num = 4 in
             fibo val",
         );
@@ -657,16 +647,13 @@ Assume(#alwaysTrue, false)
     #[test]
     fn flat_higher_order_contract() {
         let res = eval_string(
-            "let alwaysTrue = fun l t =>
-              let boolT = Assume(Bool, t) in
-              if boolT then boolT else %blame% l
-            in
-            let alwaysFalse = fun l t =>
-              let boolT = Assume(Bool, t) in
-              if boolT then %blame% l else boolT
-            in
-            let not = fun b => if b then false else true in
-            Assume(#alwaysTrue -> #alwaysFalse, not ) true",
+            "let alwaysTrue = fun l t => let boolT = Assume(Bool, t) in
+    if boolT then boolT else blame l in
+let alwaysFalse = fun l t => let boolT = Assume(Bool, t) in
+    if boolT then  blame l else boolT in
+let not = fun b => if b then false else true in
+Assume(#alwaysTrue -> #alwaysFalse, not ) true
+",
         );
 
         assert_eq!(Ok(Term::Bool(false)), res);
@@ -801,24 +788,22 @@ Assume(#alwaysTrue, false)
     #[test]
     fn records_prims() {
         assert_eq!(
-            eval_string("%hasField% \"foo\" { foo = 1; bar = 2; }"),
+            eval_string("hasField \"foo\" { foo = 1; bar = 2; }"),
             Ok(Term::Bool(true))
         );
         assert_eq!(
-            eval_string("%hasField% \"fop\" { foo = 1; bar = 2; }"),
+            eval_string("hasField \"fop\" { foo = 1; bar = 2; }"),
             Ok(Term::Bool(false))
         );
 
         assert_eq!(
-            eval_string(
-                "(%recordMap% (fun y => fun x => x + 1) { foo = 1; bar = \"it's lazy\"; }).foo"
-            ),
+            eval_string("(mapRec (fun y => fun x => x + 1) { foo = 1; bar = \"it's lazy\"; }).foo"),
             Ok(Term::Num(2.)),
         );
         assert_eq!(
             eval_string(
-                "let r = %recordMap%
-                    (fun y x => if %isNum% x then x + 1 else 0)
+                "let r = mapRec
+                    (fun y x => if isNum x then x + 1 else 0)
                     { foo = 1; bar = \"it's lazy\"; }
                 in
                 (r.foo) + (r.bar)"
@@ -827,12 +812,12 @@ Assume(#alwaysTrue, false)
         );
 
         assert_eq!(
-            eval_string("%hasField% \"foo\" ( { foo = 2; bar = 3; }-$(\"foo\"))"),
+            eval_string("hasField \"foo\" ( { foo = 2; bar = 3; }-$(\"foo\"))"),
             Ok(Term::Bool(false))
         );
 
         assert_eq!(
-            eval_string("%hasField% \"foo\" ( { bar = 3; }$[\"foo\" = 1])"),
+            eval_string("hasField \"foo\" ( { bar = 3; }$[\"foo\" = 1])"),
             Ok(Term::Bool(true))
         );
         assert_eq!(
@@ -845,22 +830,22 @@ Assume(#alwaysTrue, false)
     /// just that the evaluation succeeds
     #[test]
     fn seq_expressions() {
-        assert_eq!(eval_string("%seq% 1 true"), Ok(Term::Bool(true)));
+        assert_eq!(eval_string("seq 1 true"), Ok(Term::Bool(true)));
         assert_eq!(
-            eval_string("let x = (1 + 1) in %seq% x x"),
+            eval_string("let x = (1 + 1) in seq x x"),
             Ok(Term::Num(2.0))
         );
 
         assert_eq!(
-            eval_string("let r = {a=(1 + 1);} in %deepSeq% r (r.a)"),
+            eval_string("let r = {a=(1 + 1);} in deepSeq r (r.a)"),
             Ok(Term::Num(2.0))
         );
         assert_eq!(
-            eval_string("let r = {a=(1 + 1);b=(\"a\" ++ \"b\");} in %deepSeq% r (r.b)"),
+            eval_string("let r = {a=(1 + 1);b=(\"a\" ++ \"b\");} in deepSeq r (r.b)"),
             Ok(Term::Str(String::from("ab")))
         );
         assert_eq!(
-            eval_string("let r = {a={b=(1 + 1);};} in %deepSeq% r ((r.a).b)"),
+            eval_string("let r = {a={b=(1 + 1);};} in deepSeq r ((r.a).b)"),
             Ok(Term::Num(2.0))
         );
 
@@ -868,7 +853,7 @@ Assume(#alwaysTrue, false)
             eval_string(
                 "let inj = fun x => {b=(x + 2);} in
                 let cat = fun x => fun y => x ++ y in
-                let r = {a=(inj 1);b=(cat \"a\" \"b\");} in %deepSeq% r ((r.a).b)"
+                let r = {a=(inj 1);b=(cat \"a\" \"b\");} in deepSeq r ((r.a).b)"
             ),
             Ok(Term::Num(3.0))
         )
@@ -876,49 +861,49 @@ Assume(#alwaysTrue, false)
 
     #[test]
     fn lists() {
-        assert_eq!(eval_string("%elemAt% [1,2,3] 1"), Ok(Term::Num(2.0)));
+        assert_eq!(eval_string("elemAt [1,2,3] 1"), Ok(Term::Num(2.0)));
         assert_eq!(
-            eval_string("%elemAt% (%map% (fun x => x + 1) [1,2,3]) 1"),
+            eval_string("elemAt (map (fun x => x + 1) [1,2,3]) 1"),
             Ok(Term::Num(3.0))
         );
 
-        eval_string("%elemAt% [1,2,3] (-1)").unwrap_err();
-        eval_string("%elemAt% [1,2,3] 4").unwrap_err();
+        eval_string("elemAt [1,2,3] (-1)").unwrap_err();
+        eval_string("elemAt [1,2,3] 4").unwrap_err();
 
-        assert_eq!(eval_string("%length% []"), Ok(Term::Num(0.0)));
-        assert_eq!(eval_string("%length% [1,2,3]"), Ok(Term::Num(3.0)));
+        assert_eq!(eval_string("length []"), Ok(Term::Num(0.0)));
+        assert_eq!(eval_string("length [1,2,3]"), Ok(Term::Num(3.0)));
 
         assert_eq!(
-            eval_string("%length% ([] @ [1,2] @ [3,4] @ [])"),
+            eval_string("length ([] @ [1,2] @ [3,4] @ [])"),
             Ok(Term::Num(4.0))
         );
         // Test case added after https://github.com/tweag/nickel/issues/154
         assert_eq!(
-            eval_string("let x = 1 in let l = [x] @ [2] in %head% l"),
+            eval_string("let x = 1 in let l = [x] @ [2] in head l"),
             Ok(Term::Num(1.0))
         );
 
         assert_eq!(
-            eval_string("%head% [\"a\",\"b\",\"c\"]"),
+            eval_string("head [\"a\",\"b\",\"c\"]"),
             Ok(Term::Str(String::from("a")))
         );
-        eval_string("%head% []").unwrap_err();
+        eval_string("head []").unwrap_err();
 
         assert_eq!(
-            eval_string("%length% (%tail% [true,false,1])"),
+            eval_string("length (tail [true,false,1])"),
             Ok(Term::Num(2.0))
         );
-        eval_string("%tail% []").unwrap_err();
+        eval_string("tail []").unwrap_err();
 
         assert_eq!(
             eval_string(
                 "let Y = fun f => (fun x => f (x x)) (fun x => f (x x)) in
                 let foldr_ =
                     fun self => fun f => fun acc => fun l =>
-                        if %length% l == 0 then acc
+                        if isZero (length l) then acc
                         else
-                            let h = %head% l in
-                            let t = %tail% l in
+                            let h = head l in
+                            let t = tail l in
                             let next_acc = self f acc t in
                             f next_acc h
                 in
@@ -929,8 +914,8 @@ Assume(#alwaysTrue, false)
                             if y then true else false
                         else false
                 in
-                let all = fun pred => fun l => foldr and true (%map% pred l) in
-                let isZ = fun x => x == 0 in
+                let all = fun pred => fun l => foldr and true (map pred l) in
+                let isZ = fun x => isZero x in
                 all isZ [0, 0, 0, 1]"
             ),
             Ok(Term::Bool(false))
@@ -1016,7 +1001,7 @@ Assume(#alwaysTrue, false)
     #[test]
     fn enriched_terms_thunk_update() {
         assert_eq!(
-            eval_string("let x = {a=(fun x => Default(1)) 1} in %seq% (x.a) ((x & {a=2}).a)"),
+            eval_string("let x = {a=(fun x => Default(1)) 1} in seq (x.a) ((x & {a=2}).a)"),
             Ok(Term::Num(2.0))
         );
     }
@@ -1078,26 +1063,26 @@ Assume(#alwaysTrue, false)
              let or = fun x => fun y => if x then x else y in
              let isEven_ = Y (fun f =>
                  (fun x =>
-                     if x == 0 then true
+                     if (isZero x) then true
                      else (
-                         if dec x == 0 then false
+                         if (isZero (dec x)) then false
                          else (f (dec (dec x)))
                      )
                  )
              ) in
              let isDivBy3_ = Y (fun f =>
                  (fun x =>
-                     if x == 0 then true
+                     if (isZero x) then true
                      else (
-                         if or (dec (dec x) == 0) (dec x == 0) then false
+                         if or (isZero (dec (dec x))) (isZero (dec x)) then false
                          else (f (dec (dec (dec x))))
                      )
                  )
              ) in
              let toCtr = fun f => fun l => fun x => (
-               if (%isNum% x) then (
-                 if (f x) then x else %blame% l)
-               else %blame% l
+               if (isNum x) then (
+                 if (f x) then x else blame l)
+               else blame l
              ) in
              let isEven = toCtr isEven_ in
              let isDivBy3 = toCtr isDivBy3_ in
@@ -1209,12 +1194,12 @@ Assume(#alwaysTrue, false)
             Ok(Term::Num(3.0))
         );
         assert_eq!(
-            eval_string("{f = fun x y => if x == 0 then y else f (x + (-1)) (y + 1)}.f 5 5"),
+            eval_string("{f = fun x y => if isZero x then y else f (x + (-1)) (y + 1)}.f 5 5"),
             Ok(Term::Num(10.0))
         );
         assert_eq!(
             eval_string("
-                let with_res = fun res => { f = fun x => if x == 0 then res else g x; g = fun y => f (y + (-1)) }.f 10 in
+                let with_res = fun res => { f = fun x => if isZero x then res else g x; g = fun y => f (y + (-1)) }.f 10 in
                 with_res \"done\""),
             Ok(Term::Str(String::from("done")))
         );
@@ -1307,40 +1292,13 @@ Assume(#alwaysTrue, false)
         assert_npeq!("{ a = { a = true } }", "{a = { a = { a = true } } }");
     }
 
-    // Now that the equality operator directly uses the stack to store its continuation (see
-    // https://github.com/tweag/nickel/pull/247), check that it correctly cleans the stack when
-    // evaluating a subequality to `false`.
-    #[test]
-    fn poly_eq_nested() {
-        // Generate an non-empty evaluation context to evaluate equalities over a non-empty stack
-        let with_context = |t1, t2| {
-            format!("let not = fun b => if b then true else false in not (not (not (not (({}) == ({})))))", t1, t2)
-        };
-
-        assert_peq!(
-            with_context(
-                "{a = 1 + 0; b = 1 + 1; c = 0; d = 0}",
-                "{ a = 1; b = 3; c = 0; d = 0}"
-            ),
-            "false"
-        );
-
-        assert_peq!(
-            with_context(
-                "[[1,2,3,4], [1,0,3,4], [1,2,3,4], [1,2,3,4]]",
-                "[[1,2,3,4], [1,2,3,4], [1,2,3,4], [1,2,3,4]]"
-            ),
-            "false"
-        );
-    }
-
     #[test]
     fn fields_of() {
-        assert_peq!("%fieldsOf% {}", "[]");
-        assert_peq!("%fieldsOf% {a = 1; b = 2; c = 3}", "[\"a\", \"b\", \"c\"]");
-        assert_peq!("%fieldsOf% {aAa = 1; Zzz = 2;}", "[\"Zzz\", \"aAa\"]");
+        assert_peq!("fieldsOf {}", "[]");
+        assert_peq!("fieldsOf {a = 1; b = 2; c = 3}", "[\"a\", \"b\", \"c\"]");
+        assert_peq!("fieldsOf {aAa = 1; Zzz = 2;}", "[\"Zzz\", \"aAa\"]");
         assert_peq!(
-            "%fieldsOf% {foo = {bar = 0}; baz = Default(true)}",
+            "fieldsOf {foo = {bar = 0}; baz = Default(true)}",
             "[\"baz\", \"foo\"]"
         );
     }
@@ -1388,22 +1346,16 @@ Assume(#alwaysTrue, false)
 
     #[test]
     fn boolean_op() {
-        assert_peq!("1+1>1 && %isStr% 0", "false");
-        assert_peq!("-1 < -2 && %isFun% (fun x => x)", "false");
-        assert_peq!(
-            "%isNum% 0 && %isFun% (fun x => x) || 1 == 0 && true",
-            "true"
-        );
+        assert_peq!("1+1>1 && isStr 0", "false");
+        assert_peq!("-1 < -2 && isFun (fun x => x)", "false");
+        assert_peq!("isNum 0 && isFun (fun x => x) || 1 == 0 && true", "true");
         assert_peq!(
-            "%isNum% 0 && %isFun% false || 1 == 0 && false || 1 > 2 && 2 < 1",
+            "isNum 0 && isFun false || 1 == 0 && false || 1 > 2 && 2 < 1",
             "false"
         );
+        assert_peq!("!(isNum true) && !(isFun 0) && !(isBool \"a\")", "true");
         assert_peq!(
-            "!(%isNum% true) && !(%isFun% 0) && !(%isBool% \"a\")",
-            "true"
-        );
-        assert_peq!(
-            "!(%isNum% (fun x => x) || %isBool% (fun x => x) || %isFun% (fun x => x))",
+            "!(isNum (fun x => x) || isBool (fun x => x) || isFun (fun x => x))",
             "false"
         );
 
@@ -1427,33 +1379,35 @@ Assume(#alwaysTrue, false)
         eval_string("Assume({}, {a=1})").unwrap_err();
 
         assert_peq!(
-            "let x = Assume({a: Num, s: Str}, {a = 1; s = \"a\"}) in %deepSeq% x x",
+            "let x = Assume({a: Num, s: Str}, {a = 1; s = \"a\"}) in deepSeq x x",
             "{a = 1; s = \"a\"}"
         );
-        eval_string("let x = Assume({a: Num, s: Str}, {a = 1; s = 2}) in %deepSeq% x x")
+        eval_string("let x = Assume({a: Num, s: Str}, {a = 1; s = 2}) in deepSeq x x").unwrap_err();
+        eval_string("let x = Assume({a: Num, s: Str}, {a = \"a\"; s = \"b\"}) in deepSeq x x")
             .unwrap_err();
-        eval_string("let x = Assume({a: Num, s: Str}, {a = \"a\"; s = \"b\"}) in %deepSeq% x x")
-            .unwrap_err();
-        eval_string("let x = Assume({a: Num, s: Str}, {a = 1}) in %deepSeq% x x").unwrap_err();
-        eval_string("let x = Assume({a: Num, s: Str}, {s = \"a\"}) in %deepSeq% x x").unwrap_err();
+        eval_string("let x = Assume({a: Num, s: Str}, {a = 1}) in deepSeq x x").unwrap_err();
+        eval_string("let x = Assume({a: Num, s: Str}, {s = \"a\"}) in deepSeq x x").unwrap_err();
         eval_string(
-            "let x = Assume({a: Num, s: Str}, {a = 1; s = \"a\"; extra = 1}) in %deepSeq% x x",
+            "let x = Assume({a: Num, s: Str}, {a = 1; s = \"a\"; extra = 1}) in deepSeq x x",
         )
         .unwrap_err();
 
         assert_peq!(
-            "let x = Assume({a: Num, s: {foo: Bool}}, {a = 1; s = { foo = true}}) in %deepSeq% x x",
+            "let x = Assume({a: Num, s: {foo: Bool}}, {a = 1; s = { foo = true}}) in deepSeq x x",
             "{a = 1; s = { foo = true}}"
         );
         eval_string(
-            "let x = Assume({a: Num, s: {foo: Bool} }, {a = 1; s = { foo = 2}}) in %deepSeq% x x",
+            "let x = Assume({a: Num, s: {foo: Bool} }, {a = 1; s = { foo = 2}}) in deepSeq x x",
         )
         .unwrap_err();
-        eval_string("let x = Assume({a: Num, s: {foo: Bool} }, {a = 1; s = { foo = true; extra = 1}}) in %deepSeq% x x").unwrap_err();
-        eval_string("let x = Assume({a: Num, s: {foo: Bool} }, {a = 1; s = { }}) in %deepSeq% x x")
+        eval_string("let x = Assume({a: Num, s: {foo: Bool} }, {a = 1; s = { foo = true; extra = 1}}) in deepSeq x x").unwrap_err();
+        eval_string("let x = Assume({a: Num, s: {foo: Bool} }, {a = 1; s = { }}) in deepSeq x x")
             .unwrap_err();
     }
 
+    #[test]
+    fn records_contracts_dyn() {}
+
     #[test]
     fn records_contracts_poly() {
         let id = "let f = Assume(forall a. { | a} -> { | a }, fun x => x) in f";
@@ -1513,23 +1467,6 @@ Assume(#alwaysTrue, false)
         .unwrap_err();
     }
 
-    #[test]
-    fn records_contracts_dyn() {
-        assert_peq!(
-            "Assume({a: Num, b: Str | Dyn}, {a = 1; b = \"b\"})",
-            "{a = 1; b = \"b\"}"
-        );
-        assert_peq!(
-            "Assume({a: Num, b: Str | Dyn}, {a = 1; b = \"b\"; c = false})",
-            "{a = 1; b = \"b\"; c = false}"
-        );
-        assert_peq!(
-            "Assume({a: Num | Dyn} -> Dyn, fun r => r.b) {a = 1; b = 2}",
-            "2"
-        );
-        eval_string("Assume({a: Num, b: Str | Dyn}, {a = 1})").unwrap_err();
-    }
-
     #[test]
     fn multiline_string_indent() {
         // /!\ Trailing spaces on the first line are on purpose, don't remove ! /!\
diff --git a/src/serialize.rs b/src/serialize.rs
index a627a84a..01270463 100644
--- a/src/serialize.rs
+++ b/src/serialize.rs
@@ -1,34 +1,10 @@
 //! Serialization of an evaluated program to various data format.
 use crate::error::SerializationError;
 use crate::identifier::Ident;
-use crate::label::Label;
 use crate::term::{MetaValue, RichTerm, Term};
-use crate::types::Types;
 use serde::ser::{Error, Serialize, SerializeMap, Serializer};
 use std::collections::HashMap;
 
-/// Serializer for docstring. Ignore the meta-data and serialize the underlying term.
-pub fn serialize_docstring<S>(_doc: &String, t: &RichTerm, serializer: S) -> Result<S::Ok, S::Error>
-where
-    S: Serializer,
-{
-    t.serialize(serializer)
-}
-
-/// Serializer for a contract with a default value. Ignore the meta-data and serialize the
-/// underlying term.
-pub fn serialize_contract_default<S>(
-    _ty: &Types,
-    _l: &Label,
-    t: &RichTerm,
-    serializer: S,
-) -> Result<S::Ok, S::Error>
-where
-    S: Serializer,
-{
-    t.serialize(serializer)
-}
-
 /// Serializer for metavalues.
 pub fn serialize_meta_value<S>(meta: &MetaValue, serializer: S) -> Result<S::Ok, S::Error>
 where
@@ -72,6 +48,7 @@ impl Serialize for RichTerm {
 /// Check that a term is serializable. Serializable terms are booleans, numbers, strings, enum,
 /// lists of serializable terms or records of serializable terms.
 pub fn validate(t: &RichTerm) -> Result<(), SerializationError> {
+    use crate::term;
     use Term::*;
 
     match t.term.as_ref() {
@@ -84,7 +61,10 @@ pub fn validate(t: &RichTerm) -> Result<(), SerializationError> {
             vec.iter().try_for_each(validate)?;
             Ok(())
         }
-        DefaultValue(ref t) | ContractWithDefault(_, _, ref t) | Docstring(_, ref t) => validate(t),
+        //TODO: have a specific error for such missing value.
+        MetaValue(term::MetaValue {
+            value: Some(ref t), ..
+        }) => validate(t),
         _ => Err(SerializationError::NonSerializable(t.clone())),
     }
 }
diff --git a/src/stack.rs b/src/stack.rs
index 23e8a18b..c8e1e71f 100644
--- a/src/stack.rs
+++ b/src/stack.rs
@@ -10,14 +10,6 @@ use std::rc::Weak;
 /// An element of the stack.
 #[derive(Debug)]
 pub enum Marker {
-    /// An equality to test.
-    ///
-    /// When evaluating one equality `t1 == t2`, the abstract machine may generate several new
-    /// equalities to test (for example, take `t1` and `t2` to be `[1, 2, 3]`). In this case, the
-    /// first equality is evaluated and the remaining ones - the continuation of the whole
-    /// computation - are put on the stack as `Eq` elements. If an equality evaluates to `false` at
-    /// some point, all the consecutive `Eq` elements at the top of the stack are discarded.
-    Eq(Closure, Closure),
     /// An argument of an application.
     Arg(Closure, Option<RawSpan>),
     /// A thunk, which is pointer to a mutable memory cell to be updated.
@@ -34,28 +26,24 @@ impl Marker {
     pub fn is_arg(&self) -> bool {
         match *self {
             Marker::Arg(_, _) => true,
-            _ => false,
+            Marker::Thunk(_) => false,
+            Marker::Cont(_, _, _) => false,
         }
     }
 
     pub fn is_thunk(&self) -> bool {
         match *self {
+            Marker::Arg(_, _) => false,
             Marker::Thunk(_) => true,
-            _ => false,
+            Marker::Cont(_, _, _) => false,
         }
     }
 
     pub fn is_cont(&self) -> bool {
         match *self {
+            Marker::Arg(_, _) => false,
+            Marker::Thunk(_) => false,
             Marker::Cont(_, _, _) => true,
-            _ => false,
-        }
-    }
-
-    pub fn is_eq(&self) -> bool {
-        match *self {
-            Marker::Eq(..) => true,
-            _ => false,
         }
     }
 }
@@ -111,16 +99,6 @@ impl Stack {
         self.0.push(Marker::Cont(cont, len, pos))
     }
 
-    /// Push a sequence of equalities on the stack.
-    pub fn push_eqs<I>(&mut self, it: I)
-    where
-        I: Iterator<Item = (Closure, Closure)>,
-    {
-        self.0.extend(it.map(|(t1, t2)| Marker::Eq(t1, t2)));
-    }
-
-    /// Try to pop an argument from the top of the stack. If `None` is returned, the top element
-    /// was not an argument and the stack is left unchanged.
     pub fn pop_arg(&mut self) -> Option<(Closure, Option<RawSpan>)> {
         match self.0.pop() {
             Some(Marker::Arg(arg, pos)) => Some((arg, pos)),
@@ -132,8 +110,6 @@ impl Stack {
         }
     }
 
-    /// Try to pop a thunk from the top of the stack. If `None` is returned, the top element was
-    /// not a thunk and the stack is left unchanged.
     pub fn pop_thunk(&mut self) -> Option<Weak<RefCell<Closure>>> {
         match self.0.pop() {
             Some(Marker::Thunk(thunk)) => Some(thunk),
@@ -145,8 +121,6 @@ impl Stack {
         }
     }
 
-    /// Try to pop an operator continuation from the top of the stack. If `None` is returned, the
-    /// top element was not an operator continuation and the stack is left unchanged.
     pub fn pop_op_cont(&mut self) -> Option<(OperationCont, usize, Option<RawSpan>)> {
         match self.0.pop() {
             Some(Marker::Cont(cont, len, pos)) => Some((cont, len, pos)),
@@ -158,19 +132,6 @@ impl Stack {
         }
     }
 
-    /// Try to pop an equality from the top of the stack. If `None` is returned, the top element
-    /// was not an equality and the stack is left unchanged.
-    pub fn pop_eq(&mut self) -> Option<(Closure, Closure)> {
-        if self.0.last().map(Marker::is_eq).unwrap_or(false) {
-            match self.0.pop() {
-                Some(Marker::Eq(c1, c2)) => Some((c1, c2)),
-                _ => panic!(),
-            }
-        } else {
-            None
-        }
-    }
-
     /// Check if the top element is an argument.
     pub fn is_top_thunk(&self) -> bool {
         self.0.last().map(Marker::is_thunk).unwrap_or(false)
@@ -180,12 +141,6 @@ impl Stack {
     pub fn is_top_cont(&self) -> bool {
         self.0.last().map(Marker::is_cont).unwrap_or(false)
     }
-
-    /// Discard all the consecutive equality from the top of the stack. This drops the continuation
-    /// of the equality being currently evaluated.
-    pub fn clear_eqs(&mut self) {
-        while self.pop_eq().is_some() {}
-    }
 }
 
 #[cfg(test)]
@@ -211,7 +166,7 @@ mod tests {
     }
 
     fn some_cont() -> OperationCont {
-        OperationCont::Op1(UnaryOp::IsNum(), None)
+        OperationCont::Op1(UnaryOp::IsZero(), None)
     }
 
     fn some_arg_marker() -> Marker {
diff --git a/src/stdlib.rs b/src/stdlib.rs
index 6832a35d..4ff6435a 100644
--- a/src/stdlib.rs
+++ b/src/stdlib.rs
@@ -1,12 +1,23 @@
 //! Load the Nickel standard library in strings at compile-time.
 
+use crate::identifier::Ident;
 use crate::term::make as mk_term;
-use crate::term::RichTerm;
+use crate::term::{RichTerm, UnaryOp};
 
-pub const BUILTINS: &str = include_str!("../stdlib/builtins.ncl");
 pub const CONTRACTS: &str = include_str!("../stdlib/contracts.ncl");
 pub const LISTS: &str = include_str!("../stdlib/lists.ncl");
-pub const RECORDS: &str = include_str!("../stdlib/records.ncl");
+
+/// Accessors to the lists standard library.
+pub mod lists {
+    use super::*;
+
+    pub fn all() -> RichTerm {
+        mk_term::op1(
+            UnaryOp::StaticAccess(Ident::from("all")),
+            mk_term::var("lists"),
+        )
+    }
+}
 
 /// Accessors to the builtin contracts.
 pub mod contracts {
@@ -37,6 +48,5 @@ pub mod contracts {
     generate_accessor!(dyn_record);
     generate_accessor!(record_extend);
     generate_accessor!(forall_tail);
-    generate_accessor!(dyn_tail);
     generate_accessor!(empty_tail);
 }
diff --git a/src/term.rs b/src/term.rs
index 3add8cb7..a96ea54c 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -126,36 +126,9 @@ pub enum Term {
     #[serde(skip)]
     Wrapped(i32, RichTerm),
 
-    /// A contract. Enriched value.
-    ///
-    /// A contract at the term level. This contract is enforced when merged with a value.
-    #[serde(skip)]
-    Contract(Types, Label),
-
-    /// A default value. Enriched value.
-    ///
-    /// An enriched term representing a default value. It is dropped as soon as it is merged with a
-    /// concrete value. Otherwise, if it lives long enough to be accessed, it evaluates to the
-    /// underlying term.
-    #[serde(skip_deserializing)]
-    DefaultValue(RichTerm),
-
-    /// A contract with combined with default value. Enriched value.
-    ///
-    /// This is a combination generated during evaluation, when merging a contract and a default
-    /// value, as both need to be remembered.
-    #[serde(serialize_with = "crate::serialize::serialize_contract_default")]
-    #[serde(skip_deserializing)]
-    ContractWithDefault(Types, Label, RichTerm),
-
     #[serde(serialize_with = "crate::serialize::serialize_meta_value")]
     MetaValue(MetaValue),
 
-    /// A term together with its documentation string. Enriched value.
-    #[serde(serialize_with = "crate::serialize::serialize_docstring")]
-    #[serde(skip_deserializing)]
-    Docstring(String, RichTerm),
-
     /// An unresolved import.
     #[serde(skip)]
     Import(String),
@@ -207,14 +180,8 @@ pub enum StrChunk<E> {
     ),
 }
 
+#[cfg(test)]
 impl<E> StrChunk<E> {
-    pub fn literal<S>(s: S) -> Self
-    where
-        S: Into<String>,
-    {
-        StrChunk::Literal(s.into())
-    }
-
     pub fn expr(e: E) -> Self {
         StrChunk::Expr(e, 0)
     }
@@ -250,24 +217,13 @@ impl Term {
                 func(t1);
                 func(t2)
             }
-            Bool(_)
-            | Num(_)
-            | Str(_)
-            | Lbl(_)
-            | Var(_)
-            | Sym(_)
-            | Enum(_)
-            | Contract(_, _)
-            | Import(_)
+            Bool(_) | Num(_) | Str(_) | Lbl(_) | Var(_) | Sym(_) | Enum(_) | Import(_)
             | ResolvedImport(_) => {}
             Fun(_, ref mut t)
             | Op1(_, ref mut t)
             | Promise(_, _, ref mut t)
             | Assume(_, _, ref mut t)
-            | Wrapped(_, ref mut t)
-            | DefaultValue(ref mut t)
-            | Docstring(_, ref mut t)
-            | ContractWithDefault(_, _, ref mut t) => {
+            | Wrapped(_, ref mut t) => {
                 func(t);
             }
             MetaValue(ref mut meta) => {
@@ -313,11 +269,7 @@ impl Term {
             Term::List(_) => Some("List"),
             Term::Sym(_) => Some("Sym"),
             Term::Wrapped(_, _) => Some("Wrapped"),
-            Term::Contract(_, _)
-            | Term::ContractWithDefault(_, _, _)
-            | Term::Docstring(_, _)
-            | Term::DefaultValue(_)
-            | Term::MetaValue(_) => Some("Metavalue"),
+            Term::MetaValue(_) => Some("Metavalue"),
             Term::Let(_, _, _)
             | Term::App(_, _)
             | Term::Var(_)
@@ -358,13 +310,6 @@ impl Term {
             Term::List(_) => String::from("[ ... ]"),
             Term::Sym(_) => String::from("<sym>"),
             Term::Wrapped(_, _) => String::from("<wrapped>"),
-            Term::Contract(_, _) => String::from("<enriched:contract>"),
-            Term::ContractWithDefault(_, _, ref t) => {
-                format!("<enriched:contract,default={}>", (*t.term).shallow_repr())
-            }
-            Term::Docstring(_, ref t) => {
-                format!("<enriched:doc,term={}>", (*t.term).shallow_repr())
-            }
             Term::MetaValue(ref meta) => {
                 let mut content = String::new();
 
@@ -388,7 +333,6 @@ impl Term {
 
                 format!("<{}{}={}>", content, value_label, value)
             }
-            Term::DefaultValue(ref t) => format!("<enriched:default={}", (*t.term).shallow_repr()),
             Term::Var(Ident(id)) => id.clone(),
             Term::Let(_, _, _)
             | Term::App(_, _)
@@ -421,11 +365,7 @@ impl Term {
             | Term::Promise(_, _, _)
             | Term::Assume(_, _, _)
             | Term::Wrapped(_, _)
-            | Term::Contract(_, _)
-            | Term::DefaultValue(_)
-            | Term::ContractWithDefault(_, _, _)
             | Term::MetaValue(_)
-            | Term::Docstring(_, _)
             | Term::Import(_)
             | Term::ResolvedImport(_)
             | Term::StrChunks(_)
@@ -436,11 +376,7 @@ impl Term {
     /// Determine if a term is an enriched value.
     pub fn is_enriched(&self) -> bool {
         match self {
-            Term::Contract(_, _)
-            | Term::DefaultValue(_)
-            | Term::ContractWithDefault(_, _, _)
-            | Term::Docstring(_, _)
-            | Term::MetaValue(_) => true,
+            Term::MetaValue(_) => true,
             Term::Bool(_)
             | Term::Num(_)
             | Term::Str(_)
@@ -488,11 +424,7 @@ impl Term {
             | Term::Promise(_, _, _)
             | Term::Assume(_, _, _)
             | Term::Wrapped(_, _)
-            | Term::Contract(_, _)
-            | Term::DefaultValue(_)
-            | Term::ContractWithDefault(_, _, _)
             | Term::MetaValue(_)
-            | Term::Docstring(_, _)
             | Term::Import(_)
             | Term::ResolvedImport(_)
             | Term::StrChunks(_)
@@ -514,6 +446,11 @@ pub enum UnaryOp<CapturedTerm> {
     /// If-then-else.
     Ite(),
 
+    /// Test if a number is zero.
+    ///
+    /// Will be removed once there is a reasonable equality.
+    IsZero(),
+
     /// Test if a term is a numeral.
     IsNum(),
     /// Test if a term is a boolean.
@@ -557,14 +494,12 @@ pub enum UnaryOp<CapturedTerm> {
     /// Static means that the field identifier is a statically known string inside the source.
     StaticAccess(Ident),
 
-    /// Map a function on each element of a list.
-    ListMap(CapturedTerm),
     /// Map a function on a record.
     ///
     /// The mapped function must take two arguments, the name of the field as a string, and the
-    /// content of the field. `RecordMap` then replaces the content of each field by the result of the
-    /// function: i.e., `recordMap f {a=2;}` evaluates to `{a=(f "a" 2);}`.
-    RecordMap(CapturedTerm),
+    /// content of the field. `MapRec` then replaces the content of each field by the result of the
+    /// function: i.e., `mapRec f {a=2;}` evaluates to `{a=(f "a" 2);}`.
+    MapRec(CapturedTerm),
 
     /// Inverse the polarity of a label.
     ChangePolarity(),
@@ -642,11 +577,12 @@ impl<Ty> UnaryOp<Ty> {
                     .collect(),
                 op.map(f),
             ),
-            ListMap(t) => ListMap(f(t)),
-            RecordMap(t) => RecordMap(f(t)),
+            MapRec(t) => MapRec(f(t)),
 
             Ite() => Ite(),
 
+            IsZero() => IsZero(),
+
             IsNum() => IsNum(),
             IsBool() => IsBool(),
             IsStr() => IsStr(),
@@ -743,6 +679,8 @@ pub enum BinaryOp<CapturedTerm> {
     HasField(),
     /// Concatenate two lists.
     ListConcat(),
+    /// Map a function on each element of a list.
+    ListMap(),
     /// Access the n-th element of a list.
     ListElemAt(),
     /// The merge operator (see the [merge module](../merge/index.html)).
@@ -772,6 +710,7 @@ impl<Ty> BinaryOp<Ty> {
             DynAccess() => DynAccess(),
             HasField() => HasField(),
             ListConcat() => ListConcat(),
+            ListMap() => ListMap(),
             ListElemAt() => ListElemAt(),
             Merge() => Merge(),
         }
@@ -1006,52 +945,6 @@ impl RichTerm {
                     state,
                 )
             }
-            Term::Contract(ty, label) => {
-                let ty = match ty {
-                    Types(AbsType::Flat(t)) => Types(AbsType::Flat(t.traverse(f, state)?)),
-                    ty => ty,
-                };
-
-                Ok(RichTerm {
-                    term: Box::new(Term::Contract(ty, label)),
-                    pos,
-                })
-            }
-            Term::DefaultValue(t) => {
-                let t = t.traverse(f, state)?;
-                f(
-                    RichTerm {
-                        term: Box::new(Term::DefaultValue(t)),
-                        pos,
-                    },
-                    state,
-                )
-            }
-            Term::ContractWithDefault(ty, lbl, t) => {
-                let ty = match ty {
-                    Types(AbsType::Flat(t)) => Types(AbsType::Flat(t.traverse(f, state)?)),
-                    ty => ty,
-                };
-
-                let t = t.traverse(f, state)?;
-                f(
-                    RichTerm {
-                        term: Box::new(Term::ContractWithDefault(ty, lbl, t)),
-                        pos,
-                    },
-                    state,
-                )
-            }
-            Term::Docstring(s, t) => {
-                let t = t.traverse(f, state)?;
-                f(
-                    RichTerm {
-                        term: Box::new(Term::Docstring(s, t)),
-                        pos,
-                    },
-                    state,
-                )
-            }
             Term::MetaValue(meta) => {
                 let contract = meta
                     .contract
diff --git a/src/transformations.rs b/src/transformations.rs
index c47da70f..3ff3eb76 100644
--- a/src/transformations.rs
+++ b/src/transformations.rs
@@ -132,55 +132,6 @@ pub mod share_normal_form {
                     RichTerm::new(Term::MetaValue(meta), pos)
                 }
             }
-            Term::DefaultValue(t) => {
-                if should_share(&t.term) {
-                    let fresh_var = fresh_var();
-                    let inner = RichTerm {
-                        term: Box::new(Term::DefaultValue(Term::Var(fresh_var.clone()).into())),
-                        pos,
-                    };
-                    Term::Let(fresh_var, t, inner).into()
-                } else {
-                    RichTerm {
-                        term: Box::new(Term::DefaultValue(t)),
-                        pos,
-                    }
-                }
-            }
-            Term::ContractWithDefault(ty, lbl, t) => {
-                if should_share(&t.term) {
-                    let fresh_var = fresh_var();
-                    let inner = RichTerm {
-                        term: Box::new(Term::ContractWithDefault(
-                            ty,
-                            lbl,
-                            Term::Var(fresh_var.clone()).into(),
-                        )),
-                        pos,
-                    };
-                    Term::Let(fresh_var, t, inner).into()
-                } else {
-                    RichTerm {
-                        term: Box::new(Term::ContractWithDefault(ty, lbl, t)),
-                        pos,
-                    }
-                }
-            }
-            Term::Docstring(s, t) => {
-                if should_share(&t.term) {
-                    let fresh_var = fresh_var();
-                    let inner = RichTerm {
-                        term: Box::new(Term::Docstring(s, Term::Var(fresh_var.clone()).into())),
-                        pos,
-                    };
-                    Term::Let(fresh_var, t, inner).into()
-                } else {
-                    RichTerm {
-                        term: Box::new(Term::Docstring(s, t)),
-                        pos,
-                    }
-                }
-            }
             t => RichTerm {
                 term: Box::new(t),
                 pos,
diff --git a/src/typecheck.rs b/src/typecheck.rs
index 3204e1f8..823207da 100644
--- a/src/typecheck.rs
+++ b/src/typecheck.rs
@@ -56,21 +56,17 @@ use std::collections::{HashMap, HashSet};
 pub enum RowUnifError {
     /// The LHS had a binding that was missing in the RHS.
     MissingRow(Ident),
-    /// The LHS had a `Dyn` tail that was missing in the RHS.
-    MissingDynTail(),
     /// The RHS had a binding that was not in the LHS.
     ExtraRow(Ident),
-    /// The RHS had a additional `Dyn` tail.
-    ExtraDynTail(),
     /// There were two incompatible definitions for the same row.
     RowMismatch(Ident, UnifError),
     /// Tried to unify an enum row and a record row.
     RowKindMismatch(Ident, Option<TypeWrapper>, Option<TypeWrapper>),
-    /// One of the row was ill-formed (typically, a tail was neither a row, a variable nor `Dyn`).
+    /// One of the row was ill-formed (typically, a tail was neither a row nor a variable).
     ///
     /// This should probably not happen with proper restrictions on the parser and a correct
-    /// typechecking algorithm. We let it as an error for now, but it could be removed in the
-    /// future.
+    /// typechecking algorithm. We let it as an error for now, but it could be removed and turned
+    /// into a panic! in the future.
     IllformedRow(TypeWrapper),
     /// A [row constraint](./type.RowConstr.html) was violated.
     UnsatConstr(Ident, Option<TypeWrapper>),
@@ -93,9 +89,7 @@ impl RowUnifError {
     pub fn to_unif_err(self, left: TypeWrapper, right: TypeWrapper) -> UnifError {
         match self {
             RowUnifError::MissingRow(id) => UnifError::MissingRow(id, left, right),
-            RowUnifError::MissingDynTail() => UnifError::MissingDynTail(left, right),
             RowUnifError::ExtraRow(id) => UnifError::ExtraRow(id, left, right),
-            RowUnifError::ExtraDynTail() => UnifError::ExtraDynTail(left, right),
             RowUnifError::RowKindMismatch(id, tyw1, tyw2) => {
                 UnifError::RowKindMismatch(id, tyw1, tyw2)
             }
@@ -123,12 +117,8 @@ pub enum UnifError {
     ConstMismatch(usize, usize),
     /// Tried to unify two rows, but an identifier of the LHS was absent from the RHS.
     MissingRow(Ident, TypeWrapper, TypeWrapper),
-    /// Tried to unify two rows, but the `Dyn` tail of the RHS was absent from the LHS.
-    MissingDynTail(TypeWrapper, TypeWrapper),
     /// Tried to unify two rows, but an identifier of the RHS was absent from the LHS.
     ExtraRow(Ident, TypeWrapper, TypeWrapper),
-    /// Tried to unify two rows, but the `Dyn` tail of the RHS was absent from the LHS.
-    ExtraDynTail(TypeWrapper, TypeWrapper),
     /// A row was ill-formed.
     IllformedRow(TypeWrapper),
     /// Tried to unify a unification variable with a row type violating the [row
@@ -227,23 +217,12 @@ impl UnifError {
                 reporting::to_type(state, names, tyw2),
                 pos_opt,
             ),
-            UnifError::MissingDynTail(tyw1, tyw2) => TypecheckError::MissingDynTail(
-                reporting::to_type(state, names, tyw1),
-                reporting::to_type(state, names, tyw2),
-                pos_opt,
-            ),
-
             UnifError::ExtraRow(id, tyw1, tyw2) => TypecheckError::ExtraRow(
                 id,
                 reporting::to_type(state, names, tyw1),
                 reporting::to_type(state, names, tyw2),
                 pos_opt,
             ),
-            UnifError::ExtraDynTail(tyw1, tyw2) => TypecheckError::ExtraDynTail(
-                reporting::to_type(state, names, tyw1),
-                reporting::to_type(state, names, tyw2),
-                pos_opt,
-            ),
             UnifError::IllformedRow(tyw) => {
                 TypecheckError::IllformedType(reporting::to_type(state, names, tyw))
             }
@@ -567,7 +546,7 @@ fn type_check_(
             };
 
             if let TypeWrapper::Concrete(AbsType::DynRecord(rec_ty)) = root_ty.clone() {
-                // Checking for a dynamic record
+                // Checking for an dynamic record
                 stat_map
                     .into_iter()
                     .try_for_each(|(_, t)| -> Result<(), TypecheckError> {
@@ -634,9 +613,6 @@ fn type_check_(
         Term::Sym(_) => unify(state, strict, ty, mk_typewrapper::sym())
             .map_err(|err| err.to_typecheck_err(state, &rt.pos)),
         Term::Wrapped(_, t)
-        | Term::DefaultValue(t)
-        | Term::ContractWithDefault(_, _, t)
-        | Term::Docstring(_, t)
         | Term::MetaValue(MetaValue {
             contract: None,
             value: Some(t),
@@ -653,7 +629,7 @@ fn type_check_(
             let new_ty = TypeWrapper::Ptr(new_var(state.table));
             type_check_(state, envs, false, t, new_ty)
         }
-        Term::Contract(_, _) | Term::MetaValue(_) => Ok(()),
+        Term::MetaValue(_) => Ok(()),
         Term::Import(_) => unify(state, strict, ty, mk_typewrapper::dynamic())
             .map_err(|err| err.to_typecheck_err(state, &rt.pos)),
         Term::ResolvedImport(file_id) => {
@@ -682,6 +658,15 @@ fn type_check_(
 fn apparent_type(t: &Term, table: &mut UnifTable, strict: bool) -> TypeWrapper {
     match t {
         Term::Assume(ty, _, _) | Term::Promise(ty, _, _) => to_typewrapper(ty.clone()),
+        Term::MetaValue(MetaValue {
+            contract: Some((ty, _)),
+            ..
+        }) => to_typewrapper(ty.clone()),
+        Term::MetaValue(MetaValue {
+            contract: None,
+            value: Some(v),
+            ..
+        }) => apparent_type(v.as_ref(), table, strict),
         _ if strict => TypeWrapper::Ptr(new_var(table)),
         _ => mk_typewrapper::dynamic(),
     }
@@ -888,9 +873,7 @@ fn row_add(
         r = get_root(state.table, p);
     }
     match r {
-        TypeWrapper::Concrete(AbsType::RowEmpty()) | TypeWrapper::Concrete(AbsType::Dyn()) => {
-            Err(RowUnifError::MissingRow(id.clone()))
-        }
+        TypeWrapper::Concrete(AbsType::RowEmpty()) => Err(RowUnifError::MissingRow(id.clone())),
         TypeWrapper::Concrete(AbsType::RowExtend(id2, ty2, r2)) => {
             if *id == id2 {
                 Ok((ty2, *r2))
@@ -1075,14 +1058,10 @@ pub fn unify_rows(
     t2: AbsType<Box<TypeWrapper>>,
 ) -> Result<(), RowUnifError> {
     match (t1, t2) {
-        (AbsType::RowEmpty(), AbsType::RowEmpty()) | (AbsType::Dyn(), AbsType::Dyn()) => Ok(()),
-        (AbsType::RowEmpty(), AbsType::Dyn()) => Err(RowUnifError::ExtraDynTail()),
-        (AbsType::Dyn(), AbsType::RowEmpty()) => Err(RowUnifError::MissingDynTail()),
+        (AbsType::RowEmpty(), AbsType::RowEmpty()) => Ok(()),
         (AbsType::RowEmpty(), AbsType::RowExtend(ident, _, _))
-        | (AbsType::Dyn(), AbsType::RowExtend(ident, _, _)) => Err(RowUnifError::ExtraRow(ident)),
-        (AbsType::RowExtend(ident, _, _), AbsType::Dyn())
         | (AbsType::RowExtend(ident, _, _), AbsType::RowEmpty()) => {
-            Err(RowUnifError::MissingRow(ident))
+            Err(RowUnifError::ExtraRow(ident))
         }
         (AbsType::RowExtend(id, ty, t), r2 @ AbsType::RowExtend(_, _, _)) => {
             let (ty2, t2_tail) =
@@ -1342,6 +1321,8 @@ pub fn get_uop_type(
                 branches
             )
         }
+        // Num -> Bool
+        UnaryOp::IsZero() => mk_tyw_arrow!(AbsType::Num(), AbsType::Bool()),
         // forall a. a -> Bool
         UnaryOp::IsNum()
         | UnaryOp::IsBool()
@@ -1416,20 +1397,9 @@ pub fn get_uop_type(
 
             mk_tyw_arrow!(mk_tyw_record!((id.clone(), res.clone()); row), res)
         }
-        // List -> List
-        // Unify f with a -> b.
-        UnaryOp::ListMap(f) => {
-            let a = TypeWrapper::Ptr(new_var(state.table));
-            let b = TypeWrapper::Ptr(new_var(state.table));
-
-            let f_type = mk_tyw_arrow!(a.clone(), b.clone());
-            type_check_(state, envs.clone(), strict, f, f_type)?;
-
-            mk_tyw_arrow!(AbsType::List(), AbsType::List())
-        }
         // { _ : a} -> { _ : b }
         // Unify f with Str -> a -> b.
-        UnaryOp::RecordMap(f) => {
+        UnaryOp::MapRec(f) => {
             // Assuming f has type Str -> a -> b,
             // this has type DynRecord(a) -> DynRecord(b)
 
@@ -1456,11 +1426,9 @@ pub fn get_uop_type(
         UnaryOp::ListLength() => mk_tyw_arrow!(AbsType::List(), AbsType::Num()),
         // This should not happen, as ChunksConcat() is only produced during evaluation.
         UnaryOp::ChunksConcat(_, _, _) => panic!("cannot type ChunksConcat()"),
-        // BEFORE: forall rows. { rows } -> List
-        // Dyn -> List
+        // forall rows. { rows } -> List
         UnaryOp::FieldsOf() => mk_tyw_arrow!(
-            AbsType::Dyn(),
-            //mk_tyw_record!(; TypeWrapper::Ptr(new_var(state.table))),
+            mk_tyw_record!(; TypeWrapper::Ptr(new_var(state.table))),
             AbsType::List()
         ),
     })
@@ -1535,6 +1503,14 @@ pub fn get_bop_type(
         BinaryOp::HasField() => mk_tyw_arrow!(AbsType::Str(), AbsType::Dyn(), AbsType::Bool()),
         // List -> List -> List
         BinaryOp::ListConcat() => mk_tyw_arrow!(AbsType::List(), AbsType::List(), AbsType::List()),
+        // forall a b. (a -> b) -> List -> List
+        BinaryOp::ListMap() => {
+            let src = TypeWrapper::Ptr(new_var(state.table));
+            let tgt = TypeWrapper::Ptr(new_var(state.table));
+            let arrow = mk_tyw_arrow!(src, tgt);
+
+            mk_tyw_arrow!(arrow, AbsType::List(), AbsType::List())
+        }
         // List -> Num -> Dyn
         BinaryOp::ListElemAt() => mk_tyw_arrow!(AbsType::List(), AbsType::Num(), AbsType::Dyn()),
         // Dyn -> Dyn -> Dyn
@@ -1872,7 +1848,7 @@ mod tests {
 
         // We can typecheck any contract
         parse_and_typecheck(
-            "let alwaysTrue = fun l t => if t then t else %blame% l in
+            "let alwaysTrue = fun l t => if t then t else blame l in
             (fun x => x) : #alwaysTrue -> #alwaysTrue",
         )
         .unwrap();
@@ -1967,7 +1943,7 @@ mod tests {
         )
         .unwrap_err();
         parse_and_typecheck(
-            "(fun x => switch {bla => 1, ble => 2, bli => 4,} (%embed% bli x)) : <bla, ble> -> Num",
+            "(fun x => switch {bla => 1, ble => 2, bli => 4,} (embed bli x)) : <bla, ble> -> Num",
         )
         .unwrap();
 
@@ -2075,9 +2051,9 @@ mod tests {
 
     #[test]
     fn seq() {
-        parse_and_typecheck("%seq% false 1 : Num").unwrap();
-        parse_and_typecheck("(fun x y => %seq% x y) : forall a. (forall b. a -> b -> b)").unwrap();
-        parse_and_typecheck("let xDyn = false in let yDyn = 1 in (%seq% xDyn yDyn : Dyn)").unwrap();
+        parse_and_typecheck("seq false 1 : Num").unwrap();
+        parse_and_typecheck("(fun x y => seq x y) : forall a. (forall b. a -> b -> b)").unwrap();
+        parse_and_typecheck("let xDyn = false in let yDyn = 1 in (seq xDyn yDyn : Dyn)").unwrap();
     }
 
     #[test]
@@ -2094,18 +2070,16 @@ mod tests {
 
     #[test]
     fn lists_operations() {
-        parse_and_typecheck("fun l => %tail% l : List -> List").unwrap();
-        parse_and_typecheck("fun l => %head% l : List -> Dyn").unwrap();
-        parse_and_typecheck(
-            "fun f l => %map% f l : forall a. (forall b. (a -> b) -> List -> List)",
-        )
-        .unwrap();
+        parse_and_typecheck("fun l => tail l : List -> List").unwrap();
+        parse_and_typecheck("fun l => head l : List -> Dyn").unwrap();
+        parse_and_typecheck("fun f l => map f l : forall a. (forall b. (a -> b) -> List -> List)")
+            .unwrap();
         parse_and_typecheck("(fun l1 => fun l2 => l1 @ l2) : List -> List -> List").unwrap();
-        parse_and_typecheck("(fun i l => %elemAt% l i) : Num -> List -> Dyn ").unwrap();
+        parse_and_typecheck("(fun i l => elemAt l i) : Num -> List -> Dyn ").unwrap();
 
-        parse_and_typecheck("(fun l => %head% l) : forall a. (List -> a)").unwrap_err();
+        parse_and_typecheck("(fun l => head l) : forall a. (List -> a)").unwrap_err();
         parse_and_typecheck(
-            "(fun f l => %elemAt% (%map% f l) 0) : forall a. (forall b. (a -> b) -> List -> b)",
+            "(fun f l => elemAt (map f l) 0) : forall a. (forall b. (a -> b) -> List -> b)",
         )
         .unwrap_err();
     }
@@ -2161,11 +2135,11 @@ mod tests {
         // Fields in recursive records are treated in the type environment in the same way as let-bound expressions
         parse_and_typecheck("{a = 1; b = 1 + a} : {a : Num, b : Num}").unwrap();
         parse_and_typecheck(
-            "{ f = fun x => if x == 0 then 1 else 1 + (f (x + (-1)));} : {f : Num -> Num}",
+            "{ f = fun x => if isZero x then 1 else 1 + (f (x + (-1)));} : {f : Num -> Num}",
         )
         .unwrap();
         parse_and_typecheck(
-            "{ f = fun x => if x == 0 then false else 1 + (f (x + (-1)))} : {f : Num -> Num}",
+            "{ f = fun x => if isZero x then false else 1 + (f (x + (-1)))} : {f : Num -> Num}",
         )
         .unwrap_err();
     }
@@ -2209,17 +2183,4 @@ mod tests {
         );
         assert_row_conflict(res);
     }
-
-    #[test]
-    fn dynamic_row_tail() {
-        parse_and_typecheck("let r = Assume({a: Num | Dyn}, {a = 1; b = 2}) in (r.a : Num)")
-            .unwrap();
-        parse_and_typecheck("Assume({a: Num | Dyn}, {a = 1; b = 2}) : {a: Num | Dyn}").unwrap();
-        // Currently, typechecking is conservative wrt the dynamic row type, meaning it can't to a
-        // less precise type with a dynamic tail.
-        parse_and_typecheck("{a = 1; b = 2} : {a: Num | Dyn}").unwrap_err();
-        parse_and_typecheck("{a = 1} : {a: Num | Dyn}").unwrap_err();
-        parse_and_typecheck("Assume({a: Num | Dyn}, {a = 1}) : {a: Num}").unwrap_err();
-        parse_and_typecheck("{a = 1} : {a: Num | Dyn}").unwrap_err();
-    }
 }
diff --git a/src/types.rs b/src/types.rs
index 25650187..c0b2dfd2 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -137,7 +137,7 @@ impl<Ty> AbsType<Ty> {
     /// Determine if a type is a row type.
     pub fn is_row_type(&self) -> bool {
         match self {
-            AbsType::RowExtend(_, _, _) | AbsType::RowEmpty() | AbsType::Dyn() => true,
+            AbsType::RowExtend(_, _, _) | AbsType::RowEmpty() => true,
             _ => false,
         }
     }
@@ -248,7 +248,6 @@ impl Types {
                 ) -> RichTerm {
                     match &ty.0 {
                         AbsType::RowEmpty() => contracts::empty_tail(),
-                        AbsType::Dyn() => contracts::dyn_tail(),
                         AbsType::Var(id) => {
                             let (_, rt) = h
                                 .get(&id)
@@ -351,7 +350,6 @@ impl fmt::Display for Types {
                 match tail.0 {
                     AbsType::RowEmpty() => write!(f, "{}", tail),
                     AbsType::Var(_) => write!(f, " | {}", tail),
-                    AbsType::Dyn() => write!(f, " | Dyn"),
                     _ => write!(f, ", {}", tail),
                 }
             }
diff --git a/stdlib/builtins.ncl b/stdlib/builtins.ncl
deleted file mode 100644
index 2a2d6a3c..00000000
--- a/stdlib/builtins.ncl
+++ /dev/null
@@ -1,13 +0,0 @@
-{
-  builtins = {
-    isNum : Dyn -> Bool = fun x => %isNum% x;
-    isBool : Dyn -> Bool = fun x => %isBool% x;
-    isStr : Dyn -> Bool = fun x => %isStr% x;
-    isFun : Dyn -> Bool = fun x => %isFun% x;
-    isList : Dyn -> Bool = fun x => %isList% x;
-    isRecord : Dyn -> Bool = fun x => %isRecord% x;
-
-    seq : forall a. Dyn -> a -> a = fun x y => %seq% x y;
-    deepSeq : forall a. Dyn -> a -> a = fun x y => %deepSeq% x y;
-  }
-}
diff --git a/stdlib/contracts.ncl b/stdlib/contracts.ncl
index 3606bbab..c35fba4f 100644
--- a/stdlib/contracts.ncl
+++ b/stdlib/contracts.ncl
@@ -1,73 +1,71 @@
 {
-  dyn = fun l t => t;
+    dyn = fun l t => t;
 
-  num = fun l t => if %isNum% t then t else %blame% l;
+    num = fun l t => if isNum t then t else blame l;
 
-  bool = fun l t => if %isBool% t then t else %blame% l;
+    bool = fun l t => if isBool t then t else blame l;
 
-  string = fun l t => if %isStr% t then t else %blame% l;
+    string = fun l t => if isStr t then t else blame l;
 
-  list = fun l t => if %isList% t then t else %blame% l;
+    list = fun l t => if isList t then t else blame l;
 
-  func = fun s t l e =>
-      if %isFun% e then
-          (fun x => t (%goCodom% l) (e (s (%chngPol% (%goDom% l)) x)))
-      else
-          %blame% l;
+    func = fun s t l e =>
+        if isFun e then
+            (fun x => t (goCodom l) (e (s (chngPol (goDom l)) x)))
+        else
+            blame l;
 
-  forall_var = fun sy pol l t =>
-      let lPol = %polarity% l in
-      if pol == lPol then
-          %unwrap% sy t (%blame% l)
-      else
-          %wrap% sy t;
+    forall_var = fun sy pol l t =>
+        let lPol = polarity l in
+        if pol == lPol then
+            unwrap sy t (blame l)
+        else
+            wrap sy t;
 
-  fail = fun l t => %blame% (%tag% "Fail" l);
+    fail = fun l t => blame (tag "Fail" l);
 
-  row_extend = fun contr case l t =>
-      if (case t) then
-          t
-      else
-          contr (%tag% "NotRowExt" l) t;
+    row_extend = fun contr case l t =>
+        if (case t) then
+            t
+        else
+            contr (tag "NotRowExt" l) t;
 
-  record = fun cont l t =>
-      if %isRecord% t then
-          cont {} l t
-      else
-          %blame% (%tag% "not a record" l);
+    record = fun cont l t =>
+        if isRecord t then
+            cont {} l t
+        else
+            blame (tag "not a record" l);
 
-  dyn_record = fun contr l t =>
-      if %isRecord% t then
-          %recordMap% (fun _field => contr l) t
-      else
-          %blame% (%tag% "not a record" l);
+    dyn_record = fun contr l t =>
+        if isRecord t then
+            mapRec (fun _field => contr l) t
+        else
+            blame (tag "not a record" l);
 
-  record_extend = fun field contr cont acc l t =>
-      if %hasField% field t then
-          let acc = acc$[field = contr (%goField% field l) (t.$field)] in
-          let t = t -$ field in
-          cont acc l t
-      else
-          %blame% (%tag% "missing field" l);
+    record_extend = fun field contr cont acc l t =>
+        if hasField field t then
+            let acc = acc$[field = contr (goField field l) (t.$field)] in
+            let t = t -$ field in
+            cont acc l t
+        else
+            blame (tag "missing field" l);
 
-  forall_tail = fun sy pol acc l t =>
-      let magic_fld = "_%wrapped" in
-      if pol == (%polarity% l) then
-          if %hasField% magic_fld t then
-              if (t -$ magic_fld) == {} then
-                  let fail = %blame% (%tag% "polymorphic tail mismatch" l) in
-                  let inner = %unwrap% sy (t.$magic_fld) fail in
-                  acc & inner
-              else
-                  %blame% (%tag% "extra field" l)
-          else
-              %blame% (%tag% "missing polymorphic part" l)
-      else
-          acc$[magic_fld = %wrap% sy t];
+    forall_tail = fun sy pol acc l t =>
+        let magic_fld = "_%wrapped" in
+        if pol == (polarity l) then
+            if hasField magic_fld t then
+                if (t -$ magic_fld) == {} then
+                    let fail = blame (tag "polymorphic tail mismatch" l) in
+                    let inner = unwrap sy (t.$magic_fld) fail in
+                    acc & inner
+                else
+                    blame (tag "extra field" l)
+            else
+                blame (tag "missing polymorphic part" l)
+        else
+            acc$[magic_fld = wrap sy t];
 
-  dyn_tail = fun acc l t => acc & t;
-
-  empty_tail = fun acc l t =>
-      if t == {} then acc
-      else %blame% (%tag% "extra field" l);
+    empty_tail = fun acc l t =>
+        if t == {} then acc
+        else blame (tag "extra field" l);
 }
diff --git a/stdlib/lists.ncl b/stdlib/lists.ncl
index 091c41ad..6e892ade 100644
--- a/stdlib/lists.ncl
+++ b/stdlib/lists.ncl
@@ -1,31 +1,21 @@
 {
   lists = {
-    head : List -> Dyn = fun l => %head% l;
-
-    tail : List -> List = fun l => %tail% l;
-
-    length : List -> Num = fun l => %length% l;
-
-    map : (Dyn -> Dyn) -> List -> List = fun f l => %map% f l;
-
-    elemAt : List -> Num -> Dyn = fun l n => %elemAt% l n;
-
     concat : List -> List -> List = fun l1 l2 => l1 @ l2;
 
     foldl : forall a. (a -> Dyn -> a) -> a -> List -> a =
       fun f fst l =>
-        if %length% l == 0 then
+        if length l == 0 then
           fst
         else
-          let rest = foldl f fst (%tail% l) in
-          %seq% rest (f rest (%head% l));
+          let rest = foldl f fst (tail l) in
+          seq rest (f rest (head l));
 
     fold : forall a. (Dyn -> a -> a) -> List -> a -> a =
       fun f l fst =>
-        if %length% l == 0 then
+        if length l == 0 then
           fst
         else
-          f (%head% l) (fold f (%tail% l) fst);
+          f (head l) (fold f (tail l) fst);
 
     cons : Dyn -> List -> List = fun x l => [x] @ l;
 
@@ -35,7 +25,7 @@
 
     flatten : List -> List =
       fun l =>
-        fold (fun l acc => Assume(List, l) @ acc) l [];
+        fold (fun l acc => acc @ Assume(List, l)) l [];
 
     all : (Dyn -> Bool) -> List -> Bool =
       fun pred l =>
diff --git a/stdlib/records.ncl b/stdlib/records.ncl
deleted file mode 100644
index 2d35c37b..00000000
--- a/stdlib/records.ncl
+++ /dev/null
@@ -1,10 +0,0 @@
-{
-  records = {
-    map : forall a b. (Str -> a -> b) -> {_: a} -> {_: b} = fun f r => %recordMap% f r;
-
-    // TODO: change Dyn to { | Dyn} once the PR introducing open contracts lands
-    fieldsOf : Dyn -> List = fun r => %fieldsOf% r;
-
-    hasField : Str -> Dyn -> Bool = fun r field => %hasField% r field;
-  }
-}


Test patch:
diff --git a/src/parser/tests.rs b/src/parser/tests.rs
index fab08fa1..6bcb6a40 100644
--- a/src/parser/tests.rs
+++ b/src/parser/tests.rs
@@ -137,13 +137,13 @@ fn lets() {
 #[test]
 fn unary_op() {
     assert_eq!(
-        parse_without_pos("%isNum% x"),
-        mk_term::op1(UnaryOp::IsNum(), mk_term::var("x"))
+        parse_without_pos("isZero x"),
+        mk_term::op1(UnaryOp::IsZero(), mk_term::var("x"))
     );
     assert_eq!(
-        parse_without_pos("%isNum% x y"),
+        parse_without_pos("isZero x y"),
         mk_app!(
-            mk_term::op1(UnaryOp::IsNum(), mk_term::var("x")),
+            mk_term::op1(UnaryOp::IsZero(), mk_term::var("x")),
             mk_term::var("y")
         ),
     );
@@ -294,19 +294,3 @@ fn multiline_str_escape() {
         mk_single_chunk("#Hel##{lo###{"),
     );
 }
-
-#[test]
-fn line_comments() {
-    assert_eq!(
-        parse_without_pos("// 1 +\n1 + 1// + 3\n//+ 2"),
-        parse_without_pos("1 + 1")
-    );
-    assert_eq!(
-        parse_without_pos(
-            "{ // Some comment
-            field = foo; // Some description
-            } // Some other"
-        ),
-        parse_without_pos("{field = foo}")
-    );
-}