From 3dd75e5ba8d30f7dd702e46566ab94e3e56669ff Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 18 Feb 2021 14:01:00 +0100
Subject: [PATCH 01/12] Allow Insecure Protocol to prevent warnings during
 build

---
 build.sbt | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/build.sbt b/build.sbt
index 6cfb32f6a..f67276e4d 100644
--- a/build.sbt
+++ b/build.sbt
@@ -31,9 +31,9 @@ unmanagedJars in Compile += {
 }
 
 resolvers ++= Seq(
-  "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots",
-  "Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases",
-  "uuverifiers" at "http://logicrunch.research.it.uu.se/maven"
+  ("Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots").withAllowInsecureProtocol(true),
+  ("Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases").withAllowInsecureProtocol(true),
+  ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven").withAllowInsecureProtocol(true)
 )
 
 libraryDependencies ++= Seq(

From db421768faf17e321227707a14a9e129745f82b7 Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 18 Feb 2021 16:17:17 +0100
Subject: [PATCH 02/12] Bump Scala version to 2.12.13, sbt version to 1.3.0,
 and change tut to mdoc

---
 .gitignore                                           |  7 +++++++
 build.sbt                                            | 12 ++++++------
 project/build.properties                             |  2 +-
 project/plugins.sbt                                  |  2 +-
 .../solvers/princess/AbstractPrincessSolver.scala    |  4 ++--
 .../scala/inox/solvers/princess/PrincessSolver.scala |  4 ++--
 src/main/scala/inox/utils/Bijection.scala            |  2 +-
 7 files changed, 20 insertions(+), 13 deletions(-)

diff --git a/.gitignore b/.gitignore
index 1f21ce3cd..4e778c002 100644
--- a/.gitignore
+++ b/.gitignore
@@ -59,3 +59,10 @@ out-classes
 
 # VS Code
 .vscode
+
+# metals and bloop
+.bloop/
+.bsp/
+project/.bloop/
+project/metals.sbt
+project/project/
diff --git a/build.sbt b/build.sbt
index f67276e4d..11c3183f5 100644
--- a/build.sbt
+++ b/build.sbt
@@ -1,14 +1,14 @@
 name := "inox"
 
-enablePlugins(GitVersioning, TutPlugin)
+enablePlugins(GitVersioning, MdocPlugin)
 
 git.useGitDescribe := true
 
 organization := "ch.epfl.lara"
 
-scalaVersion := "2.12.8"
+scalaVersion := "2.12.13"
 
-crossScalaVersions := Seq("2.11.8", "2.12.8")
+crossScalaVersions := Seq("2.11.8", "2.12.13")
 
 scalacOptions ++= Seq(
   "-deprecation",
@@ -103,10 +103,10 @@ sourceGenerators in Compile += Def.task {
 
 lazy val genDoc = taskKey[Unit]("Typecheck and interpret the documentation")
 
-tutSourceDirectory := sourceDirectory.value / "main" / "doc"
-tutTargetDirectory := baseDirectory.value / "doc"
+mdocIn  := sourceDirectory.value / "main" / "doc"
+mdocOut := baseDirectory.value / "doc"
 
-genDoc := { tutQuick.value; () }
+genDoc := { () }
 genDoc := (genDoc dependsOn (compile in Compile)).value
 
 Keys.fork in run := true
diff --git a/project/build.properties b/project/build.properties
index c0bab0494..080a737ed 100644
--- a/project/build.properties
+++ b/project/build.properties
@@ -1 +1 @@
-sbt.version=1.2.8
+sbt.version=1.3.0
diff --git a/project/plugins.sbt b/project/plugins.sbt
index c793960e3..bd093a915 100644
--- a/project/plugins.sbt
+++ b/project/plugins.sbt
@@ -1,5 +1,5 @@
 
-addSbtPlugin("org.tpolecat" % "tut-plugin" % "0.6.11")
+addSbtPlugin("org.scalameta" % "sbt-mdoc" % "2.2.18")
 
 addSbtPlugin("com.typesafe.sbt" % "sbt-git" % "1.0.0")
 
diff --git a/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala b/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala
index 57736d1cf..49d133e27 100644
--- a/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala
+++ b/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala
@@ -142,11 +142,11 @@ trait AbstractPrincessSolver extends AbstractSolver with ADTManagers {
 
       case And(exprs) =>
         val subExprs = for (e <- exprs) yield parseFormula(e)
-        (subExprs.head /: subExprs.tail)((p, q) => p & q)
+        subExprs.tail.foldLeft(subExprs.head)((p, q) => p & q)
 
       case Or(exprs) => {
         val subExprs = for (e <- exprs) yield parseFormula(e)
-        (subExprs.head /: subExprs.tail)((p, q) => p | q)
+        subExprs.tail.foldLeft(subExprs.head)((p, q) => p | q)
       }
 
       case Implies(lhs, rhs) => {
diff --git a/src/main/scala/inox/solvers/princess/PrincessSolver.scala b/src/main/scala/inox/solvers/princess/PrincessSolver.scala
index 95d44f2a3..8c5afb93a 100644
--- a/src/main/scala/inox/solvers/princess/PrincessSolver.scala
+++ b/src/main/scala/inox/solvers/princess/PrincessSolver.scala
@@ -69,8 +69,8 @@ trait PrincessSolver extends AbstractUnrollingSolver { self =>
     private implicit def exprToFormula(iexpr: IExpression): IFormula = iexpr.asInstanceOf[IFormula]
 
     def mkNot(e: IExpression) = ! e
-    def mkAnd(es: IExpression*) = (es.head /: es.tail)((p,q) => p & q)
-    def mkOr(es: IExpression*) = (es.head /: es.tail)((p,q) => p | q)
+    def mkAnd(es: IExpression*) = es.tail.foldLeft(es.head)((p,q) => p & q)
+    def mkOr(es: IExpression*) = es.tail.foldLeft(es.head)((p,q) => p | q)
     def mkImplies(e1: IExpression, e2: IExpression) = e1 ==> e2
     def mkEquals(e1: IExpression, e2: IExpression) = (e1, e2) match {
       case (f1: IFormula, f2: IFormula) => f1 <=> f2
diff --git a/src/main/scala/inox/utils/Bijection.scala b/src/main/scala/inox/utils/Bijection.scala
index 56f5706c2..22b84491b 100644
--- a/src/main/scala/inox/utils/Bijection.scala
+++ b/src/main/scala/inox/utils/Bijection.scala
@@ -43,7 +43,7 @@ class Bijection[A, B] extends Iterable[(A, B)] {
   }
 
   def ++=(t: Iterable[(A, B)]) = {
-    (this /: t){ case (b, elem) => b += elem }
+    t.foldLeft(this){ case (b, elem) => b += elem }
   }
 
   def clear(): Unit = {

From f07926ffa4d4eed0141e5bb75715b380edae9d4f Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 18 Feb 2021 16:39:24 +0100
Subject: [PATCH 03/12] Change larabot commands for 2.12.13

---
 .larabot.conf | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.larabot.conf b/.larabot.conf
index a55b338f9..c3076d447 100644
--- a/.larabot.conf
+++ b/.larabot.conf
@@ -1,7 +1,7 @@
 commands = [
+    "sbt -batch ++2.12.13 test"
+    "sbt -batch ++2.12.13 it:test"
     "sbt -batch ++2.11.8 test"
-    "sbt -batch ++2.11.8 it:test"
-    "sbt -batch ++2.12.1 test"
 ]
 
 trusted = [

From d63c0d27a34dc094cb4f32b3517059fce2a0b5aa Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 18 Feb 2021 17:16:23 +0100
Subject: [PATCH 04/12] typo

---
 src/test/scala/inox/evaluators/EvaluatorSuite.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/scala/inox/evaluators/EvaluatorSuite.scala b/src/test/scala/inox/evaluators/EvaluatorSuite.scala
index ad26a9741..6c244174e 100644
--- a/src/test/scala/inox/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/inox/evaluators/EvaluatorSuite.scala
@@ -311,7 +311,7 @@ class EvaluatorSuite extends FunSuite {
     eval(e, Not(BooleanLiteral(true)))                            === BooleanLiteral(false)
   }
 
-  test("Real Arightmetic") {
+  test("Real Arithmetic") {
     val e = evaluator(ctx)
 
     eval(e, Plus(FractionLiteral(2, 3), FractionLiteral(1, 3))) === FractionLiteral(1, 1)

From 2c3095e9f0e8f82625b41b4870a0fce213e62b5c Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 18 Feb 2021 18:11:29 +0100
Subject: [PATCH 05/12] Remove unnecessary withAllowInsecureProtocol calls

---
 build.sbt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/build.sbt b/build.sbt
index 11c3183f5..dc8f64ad2 100644
--- a/build.sbt
+++ b/build.sbt
@@ -31,8 +31,8 @@ unmanagedJars in Compile += {
 }
 
 resolvers ++= Seq(
-  ("Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots").withAllowInsecureProtocol(true),
-  ("Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases").withAllowInsecureProtocol(true),
+  "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots",
+  "Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases",
   ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven").withAllowInsecureProtocol(true)
 )
 

From 82f6a2da0b30fd6267ea380b91db219ccb418a8b Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 18 Feb 2021 18:12:43 +0100
Subject: [PATCH 06/12] Silence exhaustive match warning

---
 src/main/scala/inox/tip/Printer.scala | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index bc732aa91..a11ec559e 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -152,9 +152,12 @@ class Printer(val program: InoxProgram, val context: Context, writer: Writer) ex
       case (ADTType(id, tps), DataType(sym, cases)) =>
         val tsort = getSort(id).typed
         (ADTType(id, tsort.definition.typeArgs), DataType(sym,
-          (tsort.constructors zip cases).map { case (tcons, Constructor(sym, ADTCons(id, tps), fields)) =>
-            Constructor(sym, ADTCons(id, tsort.definition.typeArgs),
-              (tcons.fields zip fields).map { case (vd, (id, _)) => (id, vd.getType) })
+          (tsort.constructors zip cases).map {
+            case (tcons, Constructor(sym, ADTCons(id, tps), fields)) =>
+              Constructor(sym, ADTCons(id, tsort.definition.typeArgs),
+                (tcons.fields zip fields).map { case (vd, (id, _)) => (id, vd.getType) })
+            case _ =>
+              context.reporter.internalError("match should be exhaustive")
           }))
 
       case (TupleType(tps), DataType(sym, Seq(Constructor(id, TupleCons(_), fields)))) =>

From 198e513cd8c11b24c9dd3c825a4c39feae37f94c Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 18 Feb 2021 18:13:09 +0100
Subject: [PATCH 07/12] Use mdoc in documentation

---
 doc/API.md                     |   2 +-
 doc/interpolations.md          | 174 +++++++++++++++++++++------------
 doc/trees.md                   |   2 +-
 doc/tutorial.md                |   4 +-
 src/main/doc/API.md            |   2 +-
 src/main/doc/interpolations.md |  44 ++++-----
 src/main/doc/trees.md          |   6 +-
 src/main/doc/tutorial.md       |  22 ++---
 8 files changed, 151 insertions(+), 105 deletions(-)

diff --git a/doc/API.md b/doc/API.md
index 51daaf206..0ece36515 100644
--- a/doc/API.md
+++ b/doc/API.md
@@ -1,7 +1,7 @@
 Inox API
 ========
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Trees
 -----
diff --git a/doc/interpolations.md b/doc/interpolations.md
index e98b6a23d..754fbacad 100644
--- a/doc/interpolations.md
+++ b/doc/interpolations.md
@@ -1,7 +1,7 @@
 Inox String Interpolation
 =========================
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 # Table of Content
 
@@ -44,26 +44,30 @@ import inox._
 import inox.trees._
 import inox.trees.interpolator._
 
-implicit val symbols: trees.Symbols = trees.NoSymbols
+implicit val symbols: inox.trees.Symbols = inox.trees.NoSymbols
 ```
 
 Once imported, it is possible to build Inox types and expressions using a friendlier syntax:
 
 ```scala
-scala> val tpe = t"Boolean"
-tpe: inox.trees.interpolator.trees.Type = Boolean
-
-scala> val expr = e"1 + 1 == 2"
-expr: inox.trees.interpolator.trees.Expr = 1 + 1 == 2
+val tpe = t"Boolean"
+// tpe: Type = Boolean
+val expr = e"1 + 1 == 2"
+// expr: Expr = Equals(
+//   Plus(IntegerLiteral(1), IntegerLiteral(1)),
+//   IntegerLiteral(2)
+// )
 ```
 
 It is also possible to embed types and expressions:
 
 ```scala
-scala> e"let x: $tpe = $expr in !x"
-res0: inox.trees.interpolator.trees.Expr =
-val x: Boolean = 1 + 1 == 2
-¬x
+e"let x: $tpe = $expr in !x"
+// res0: Expr = Let(
+//   ValDef(x, Boolean, List()),
+//   Equals(Plus(IntegerLiteral(1), IntegerLiteral(1)), IntegerLiteral(2)),
+//   Not(Variable(x, Boolean, List()))
+// )
 ```
 
 <a name="syntax"></a>
@@ -76,62 +80,61 @@ val x: Boolean = 1 + 1 == 2
 ### Boolean literals
 
 ```scala
-scala> e"true"
-res1: inox.trees.interpolator.trees.Expr = true
-
-scala> e"false"
-res2: inox.trees.interpolator.trees.Expr = false
+e"true"
+// res1: Expr = BooleanLiteral(true)
+e"false"
+// res2: Expr = BooleanLiteral(false)
 ```
 
 <a name="numeric-literals"></a>
 ### Numeric literal
 
 ```scala
-scala> e"1"
-res3: inox.trees.interpolator.trees.Expr = 1
+e"1"
+// res3: Expr = IntegerLiteral(1)
 ```
 
 Note that the type of numeric expressions is inferred. In case of ambiguity, `BigInt` is chosen by default.
 
 ```scala
-scala> e"1".getType
-res4: inox.trees.interpolator.trees.Type = BigInt
+e"1".getType
+// res4: Type = BigInt
 ```
 
 It is however possible to annotate the desired type.
 
 ```scala
-scala> e"1 : Int".getType
-res5: inox.trees.interpolator.trees.Type = Int
+e"1 : Int".getType
+// res5: Type = BVType(true, 32)
 ```
 
 ```scala
-scala> e"1 : Real".getType
-res6: inox.trees.interpolator.trees.Type = Real
+e"1 : Real".getType
+// res6: Type = Real
 ```
 
 <a name="real-literals"></a>
 #### Real literals
 
 ```scala
-scala> e"3.75"
-res7: inox.trees.interpolator.trees.Expr = 15/4
+e"3.75"
+// res7: Expr = FractionLiteral(15, 4)
 ```
 
 <a name="string-literals"></a>
 ### String literals
 
 ```scala
-scala> e"'Hello world!'"
-res8: inox.trees.interpolator.trees.Expr = "Hello world!"
+e"'Hello world!'"
+// res8: Expr = StringLiteral("Hello world!")
 ```
 
 <a name="character-literals"></a>
 ### Character literals
 
 ```scala
-scala> e"`a`"
-res9: inox.trees.interpolator.trees.Expr = 'a'
+e"`a`"
+// res9: Expr = CharLiteral('a')
 ```
 
 <a name="arithmetic"></a>
@@ -140,53 +143,69 @@ res9: inox.trees.interpolator.trees.Expr = 'a'
 Arithmetic operators are infix and have there usual associativity and priority.
 
 ```scala
-scala> e"1 + 2 * 5 + 6 - 7 / 17"
-res10: inox.trees.interpolator.trees.Expr = ((1 + 2 * 5) + 6) - 7 / 17
+e"1 + 2 * 5 + 6 - 7 / 17"
+// res10: Expr = Minus(
+//   Plus(
+//     Plus(IntegerLiteral(1), Times(IntegerLiteral(2), IntegerLiteral(5))),
+//     IntegerLiteral(6)
+//   ),
+//   Division(IntegerLiteral(7), IntegerLiteral(17))
+// )
 ```
 
 <a name="conditionals"></a>
 ## Conditionals
 
 ```scala
-scala> e"if (1 == 2) 'foo' else 'bar'"
-res11: inox.trees.interpolator.trees.Expr =
-if (1 == 2) {
-  "foo"
-} else {
-  "bar"
-}
+e"if (1 == 2) 'foo' else 'bar'"
+// res11: Expr = IfExpr(
+//   Equals(IntegerLiteral(1), IntegerLiteral(2)),
+//   StringLiteral("foo"),
+//   StringLiteral("bar")
+// )
 ```
 
 <a name="let-bindings"></a>
 ## Let bindings
 
 ```scala
-scala> e"let word: String = 'World!' in concatenate('Hello ', word)"
-res12: inox.trees.interpolator.trees.Expr =
-val word: String = "World!"
-"Hello " + word
+e"let word: String = 'World!' in concatenate('Hello ', word)"
+// res12: Expr = Let(
+//   ValDef(word, String, List()),
+//   StringLiteral("World!"),
+//   StringConcat(StringLiteral("Hello "), Variable(word, String, List()))
+// )
 ```
 
 <a name="lambda-expressions"></a>
 ## Lambda expressions
 
 ```scala
-scala> e"lambda x: BigInt, y: BigInt. x + y"
-res13: inox.trees.interpolator.trees.Expr = (x: BigInt, y: BigInt) => x + y
+e"lambda x: BigInt, y: BigInt. x + y"
+// res13: Expr = Lambda(
+//   List(ValDef(x, BigInt, List()), ValDef(y, BigInt, List())),
+//   Plus(Variable(x, BigInt, List()), Variable(y, BigInt, List()))
+// )
 ```
 
 It is also possible to use the Unicode `λ` symbol.
 
 ```scala
-scala> e"λx: BigInt, y: BigInt. x + y"
-res14: inox.trees.interpolator.trees.Expr = (x: BigInt, y: BigInt) => x + y
+e"λx: BigInt, y: BigInt. x + y"
+// res14: Expr = Lambda(
+//   List(ValDef(x, BigInt, List()), ValDef(y, BigInt, List())),
+//   Plus(Variable(x, BigInt, List()), Variable(y, BigInt, List()))
+// )
 ```
 
 Type annotations can be omitted for any of the parameters if their type can be inferred.
 
 ```scala
-scala> e"lambda x. x * 0.5"
-res15: inox.trees.interpolator.trees.Expr = (x: Real) => x * 1/2
+e"lambda x. x * 0.5"
+// res15: Expr = Lambda(
+//   List(ValDef(x, Real, List())),
+//   Times(Variable(x, Real, List()), FractionLiteral(1, 2))
+// )
 ```
 
 <a name="quantifiers"></a>
@@ -196,33 +215,60 @@ res15: inox.trees.interpolator.trees.Expr = (x: Real) => x * 1/2
 ### Universal Quantifier
 
 ```scala
-scala> e"forall x: Int. x > 0"
-res16: inox.trees.interpolator.trees.Expr = ∀x: Int. (x > 0)
-
-scala> e"∀x. x || true"
-res17: inox.trees.interpolator.trees.Expr = ∀x: Boolean. (x || true)
+e"forall x: Int. x > 0"
+// res16: Expr = Forall(
+//   List(ValDef(x, Int, List())),
+//   GreaterThan(
+//     Variable(x, BVType(true, 32), List()),
+//     BVLiteral(true, BitSet(), 32)
+//   )
+// )
+e"∀x. x || true"
+// res17: Expr = Forall(
+//   List(ValDef(x, Boolean, List())),
+//   Or(List(Variable(x, Boolean, List()), BooleanLiteral(true)))
+// )
 ```
 
 <a name="existential-quantifiers"></a>
 ### Existential Quantifier
 
 ```scala
-scala> e"exists x: BigInt. x < 0"
-res18: inox.trees.interpolator.trees.Expr = ¬∀x: BigInt. ¬(x < 0)
-
-scala> e"∃x, y. x + y == 0"
-res19: inox.trees.interpolator.trees.Expr = ¬∀x: BigInt, y: BigInt. (x + y ≠ 0)
+e"exists x: BigInt. x < 0"
+// res18: Expr = Not(
+//   Forall(
+//     List(ValDef(x, BigInt, List())),
+//     Not(LessThan(Variable(x, BigInt, List()), IntegerLiteral(0)))
+//   )
+// )
+e"∃x, y. x + y == 0"
+// res19: Expr = Not(
+//   Forall(
+//     List(ValDef(x, BigInt, List()), ValDef(y, BigInt, List())),
+//     Not(
+//       Equals(
+//         Plus(Variable(x, BigInt, List()), Variable(y, BigInt, List())),
+//         IntegerLiteral(0)
+//       )
+//     )
+//   )
+// )
 ```
 
 <a name="choose"></a>
 ## Choose
 
 ```scala
-scala> e"choose x. x * 3 < 17"
-res20: inox.trees.interpolator.trees.Expr = choose((x: BigInt) => x * 3 < 17)
-
-scala> e"choose x: String. true"
-res21: inox.trees.interpolator.trees.Expr = choose((x: String) => true)
+e"choose x. x * 3 < 17"
+// res20: Expr = Choose(
+//   ValDef(x, BigInt, List()),
+//   LessThan(
+//     Times(Variable(x, BigInt, List()), IntegerLiteral(3)),
+//     IntegerLiteral(17)
+//   )
+// )
+e"choose x: String. true"
+// res21: Expr = Choose(ValDef(x, String, List()), BooleanLiteral(true))
 ```
 
 <a name="primitives"></a>
diff --git a/doc/trees.md b/doc/trees.md
index f381688d9..fbdf29b55 100644
--- a/doc/trees.md
+++ b/doc/trees.md
@@ -1,7 +1,7 @@
 Extending the Trees
 ===================
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Inox trees are designed to be extensible with minimal pain and maximal gain.
 By extending the [```Trees```](/src/main/scala/inox/ast/Trees.scala) trait,
diff --git a/doc/tutorial.md b/doc/tutorial.md
index 1cfbd7ef2..2f0eb5514 100644
--- a/doc/tutorial.md
+++ b/doc/tutorial.md
@@ -1,7 +1,7 @@
 Tutorial
 ========
 
-[//]: # (The documentation source are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation source are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Let us consider the problem of checking whether the following size function on a list is always greater or equal to 0.
 ```scala
@@ -157,7 +157,7 @@ val sizeFunction = mkFunDef(size)("A") { case Seq(tp) => (
 
 A symbol table in Inox is an instance of `Symbols`. The easiest way to construct one is to use
 ```scala
-implicit val symbols: trees.Symbols = {
+implicit val symbols: inox.trees.Symbols = {
   NoSymbols
     .withFunctions(Seq(sizeFunction))
     .withSorts(Seq(listSort))
diff --git a/src/main/doc/API.md b/src/main/doc/API.md
index 51daaf206..0ece36515 100644
--- a/src/main/doc/API.md
+++ b/src/main/doc/API.md
@@ -1,7 +1,7 @@
 Inox API
 ========
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Trees
 -----
diff --git a/src/main/doc/interpolations.md b/src/main/doc/interpolations.md
index bd127260b..905c8bd7f 100644
--- a/src/main/doc/interpolations.md
+++ b/src/main/doc/interpolations.md
@@ -1,7 +1,7 @@
 Inox String Interpolation
 =========================
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 # Table of Content
 
@@ -39,24 +39,24 @@ In this document, we describe the string interpolation facility offered in Inox.
 
 The first step to use this feature is to import it. The string interpolator is located within the `Symbols` class.
 
-```tut:silent
+```scala mdoc:silent
 import inox._
 import inox.trees._
 import inox.trees.interpolator._
 
-implicit val symbols: trees.Symbols = trees.NoSymbols
+implicit val symbols: inox.trees.Symbols = inox.trees.NoSymbols
 ```
 
 Once imported, it is possible to build Inox types and expressions using a friendlier syntax:
 
-```tut
+```scala mdoc
 val tpe = t"Boolean"
 val expr = e"1 + 1 == 2"
 ```
 
 It is also possible to embed types and expressions:
 
-```tut
+```scala mdoc
 e"let x: $tpe = $expr in !x"
 ```
 
@@ -69,7 +69,7 @@ e"let x: $tpe = $expr in !x"
 <a name="boolean-literals"></a>
 ### Boolean literals
 
-```tut
+```scala mdoc
 e"true"
 e"false"
 ```
@@ -77,44 +77,44 @@ e"false"
 <a name="numeric-literals"></a>
 ### Numeric literal
 
-```tut
+```scala mdoc
 e"1"
 ```
 
 Note that the type of numeric expressions is inferred. In case of ambiguity, `BigInt` is chosen by default.
 
-```tut
+```scala mdoc
 e"1".getType
 ```
 
 It is however possible to annotate the desired type.
 
-```tut
+```scala mdoc
 e"1 : Int".getType
 ```
 
-```tut
+```scala mdoc
 e"1 : Real".getType
 ```
 
 <a name="real-literals"></a>
 #### Real literals
 
-```tut
+```scala mdoc
 e"3.75"
 ```
 
 <a name="string-literals"></a>
 ### String literals
 
-```tut
+```scala mdoc
 e"'Hello world!'"
 ```
 
 <a name="character-literals"></a>
 ### Character literals
 
-```tut
+```scala mdoc
 e"`a`"
 ```
 
@@ -123,40 +123,40 @@ e"`a`"
 
 Arithmetic operators are infix and have there usual associativity and priority.
 
-```tut
+```scala mdoc
 e"1 + 2 * 5 + 6 - 7 / 17"
 ```
 
 <a name="conditionals"></a>
 ## Conditionals
 
-```tut
+```scala mdoc
 e"if (1 == 2) 'foo' else 'bar'"
 ```
 
 <a name="let-bindings"></a>
 ## Let bindings
 
-```tut
+```scala mdoc
 e"let word: String = 'World!' in concatenate('Hello ', word)"
 ```
 
 <a name="lambda-expressions"></a>
 ## Lambda expressions
 
-```tut
+```scala mdoc
 e"lambda x: BigInt, y: BigInt. x + y"
 ```
 
 It is also possible to use the Unicode `λ` symbol.
 
-```tut
+```scala mdoc
 e"λx: BigInt, y: BigInt. x + y"
 ```
 
 Type annotations can be omitted for any of the parameters if their type can be inferred.
 
-```tut
+```scala mdoc
 e"lambda x. x * 0.5"
 ```
 
@@ -166,7 +166,7 @@ e"lambda x. x * 0.5"
 <a name="universal-quantifiers"></a>
 ### Universal Quantifier
 
-```tut
+```scala mdoc
 e"forall x: Int. x > 0"
 e"∀x. x || true"
 ```
@@ -174,7 +174,7 @@ e"∀x. x || true"
 <a name="existential-quantifiers"></a>
 ### Existential Quantifier
 
-```tut
+```scala mdoc
 e"exists x: BigInt. x < 0"
 e"∃x, y. x + y == 0"
 ```
@@ -182,7 +182,7 @@ e"∃x, y. x + y == 0"
 <a name="choose"></a>
 ## Choose
 
-```tut
+```scala mdoc
 e"choose x. x * 3 < 17"
 e"choose x: String. true"
 ```
diff --git a/src/main/doc/trees.md b/src/main/doc/trees.md
index f47053e8c..73142443f 100644
--- a/src/main/doc/trees.md
+++ b/src/main/doc/trees.md
@@ -1,12 +1,12 @@
 Extending the Trees
 ===================
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Inox trees are designed to be extensible with minimal pain and maximal gain.
 By extending the [```Trees```](/src/main/scala/inox/ast/Trees.scala) trait,
 one can introduce new `Tree` subtypes and extend the supported language.
-```tut:silent
+```scala mdoc:silent
 trait Trees extends inox.ast.Trees {
   // new Expressions and Types and stuff
 }
@@ -17,7 +17,7 @@ trait Trees extends inox.ast.Trees {
 Alongside the tree definitions, one must provide a *deconstructor* for the
 new ASTs by extending
 [`TreeDeconstructor`](/src/main/scala/inox/ast/Deconstructors.scala):
-```tut:silent
+```scala mdoc:silent
 trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
   protected val s: Trees
   protected val t: Trees
diff --git a/src/main/doc/tutorial.md b/src/main/doc/tutorial.md
index 03e8521da..d6510bd09 100644
--- a/src/main/doc/tutorial.md
+++ b/src/main/doc/tutorial.md
@@ -1,7 +1,7 @@
 Tutorial
 ========
 
-[//]: # (The documentation source are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation source are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Let us consider the problem of checking whether the following size function on a list is always greater or equal to 0.
 ```scala
@@ -16,7 +16,7 @@ However, Inox provides all the tools necessary to enable inductive reasoning, as
 
 Let us start by setting up some useful imports:
 
-```tut:silent
+```scala mdoc:silent
 import inox._
 import inox.trees._
 import inox.trees.dsl._
@@ -46,19 +46,19 @@ def mkSort(id: Identifier)
 ```
 
 We therefore start by setting up the identifiers for the `List` sort
-```tut:silent
+```scala mdoc:silent
 val list: Identifier = FreshIdentifier("List")
 val cons: Identifier = FreshIdentifier("Cons")
 val nil: Identifier = FreshIdentifier("Nil")
 ```
 It is also useful to create identifiers for the fields of ADTs, as we will see shortly
-```tut:silent
+```scala mdoc:silent
 val head: Identifier = FreshIdentifier("head")
 val tail: Identifier = FreshIdentifier("tail")
 ```
 
 Based on these, we can construct the relevant ADT sort and constructors
-```tut:silent
+```scala mdoc:silent
 val listSort = mkSort(list)("A") {
   case Seq(tp) => /* `tp` is the type parameter required by the "A" argument to `mkSort`. */
     Seq(
@@ -77,7 +77,7 @@ sorts and their constructors must have the same number of type parameters).
 ### Function Definition
 
 Let us now consider the function `size`. We start by defining the symbol corresponding to the function's definition.
-```tut:silent
+```scala mdoc:silent
 val size: Identifier = FreshIdentifier("size")
 ```
 
@@ -132,7 +132,7 @@ def mkFunDef(id: Identifier)
             (builder: Seq[TypeParameter] => (Seq[ValDef], Type, Seq[Variable] => Expr)): FunDef
 ```
 and we can then construct the function definition as
-```tut:silent
+```scala mdoc:silent
 val sizeFunction = mkFunDef(size)("A") { case Seq(tp) => (
   /* We now define the argument list of the size function.
    * Note that `"ls" :: T(list)(tp)` is a shorthand for the definition
@@ -156,8 +156,8 @@ val sizeFunction = mkFunDef(size)("A") { case Seq(tp) => (
 ### Symbols
 
 A symbol table in Inox is an instance of `Symbols`. The easiest way to construct one is to use
-```tut:silent
-implicit val symbols: trees.Symbols = {
+```scala mdoc:silent
+implicit val symbols: inox.trees.Symbols = {
   NoSymbols
     .withFunctions(Seq(sizeFunction))
     .withSorts(Seq(listSort))
@@ -184,7 +184,7 @@ It is the burden of the user to construct a sound verification procedure with th
 Sound assume/guarantee reasoning can be implemented by checking that the body of `size` (without
 the `Assume` statement) satisfies the condition we are trying to prove. (Note that termination of
 `size` is also a requirement here.) The property we are interested in is therefore
-```tut:silent
+```scala mdoc:silent
 val tp: TypeParameter = TypeParameter.fresh("A")
 val ls: Variable = Variable.fresh("ls", T(list)(tp))
 val prop = (if_ (ls is cons) {
@@ -197,7 +197,7 @@ __Note__: Inox will assume the inductive invariant on the recursive call to `siz
 
 In order to verify the property, we get an instance of an Inox solver (see
 [Programs](/doc/API.md#programs) and [Solvers](/doc/API.md#solvers) for more details):
-```tut:silent
+```scala mdoc:silent
 implicit val ctx: Context = Context.empty
 val program = inox.Program(inox.trees)(symbols)
 val solver = program.getSolver.getNewSolver

From 7ced974e162521e59b525f092748d86fe2df153e Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Fri, 19 Feb 2021 13:49:29 +0100
Subject: [PATCH 08/12] Fix line numbers in documentation

---
 src/main/doc/tutorial.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/doc/tutorial.md b/src/main/doc/tutorial.md
index d6510bd09..15d517097 100644
--- a/src/main/doc/tutorial.md
+++ b/src/main/doc/tutorial.md
@@ -25,8 +25,8 @@ import inox.solvers._
 
 The explanation is the following:
 - `inox._` imports [`InoxProgram` and many others](/src/main/scala/inox/package.scala#L19)
-- `inox.trees._` imports the content of the default implementation [`trees`](/src/main/scala/inox/package.scala#L58) extending [`Trees`](/src/main/scala/inox/ast/Trees.scala#L10).
-- `inox.trees.dsl._` imports the [domain-specific-language helpers](/src/main/scala/inox/ast/DSL.scala#L20) to create [`trees`](/src/main/scala/inox/package.scala#L58) expressions.
+- `inox.trees._` imports the content of the default implementation [`trees`](/src/main/scala/inox/package.scala#L53) extending [`Trees`](/src/main/scala/inox/ast/Trees.scala#L10).
+- `inox.trees.dsl._` imports the [domain-specific-language helpers](/src/main/scala/inox/ast/DSL.scala#L20) to create [`trees`](/src/main/scala/inox/package.scala#L53) expressions.
 - `inox.solvers._` imports the [solvers](/src/main/scala/inox/solvers/package.scala#L8).
 
 ## Creating the Symbol Table

From e1166f566241c951134a388763e41425b0152a5b Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Fri, 19 Feb 2021 13:57:19 +0100
Subject: [PATCH 09/12] Fix broken link in documentation

---
 src/main/doc/trees.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/doc/trees.md b/src/main/doc/trees.md
index 73142443f..96be85652 100644
--- a/src/main/doc/trees.md
+++ b/src/main/doc/trees.md
@@ -158,7 +158,7 @@ interfaces for such cases:
 It is sometimes useful to have a bidirectional translation between two sorts of trees.
 Inox provides a mechanism to maintain an encoder/decoder pair alongside a pair of
 source and target programs through an instance of
-[ProgramTransformer](/src/main/scala/inox/ast/ProgramEncoder.scala).
+[ProgramTransformer](/src/main/scala/inox/transformers/ProgramTransformer.scala).
 
 ## Providing new semantics
 

From afeb7bc8a35fc29effb1f44fab03f5138901b247 Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Fri, 19 Feb 2021 13:59:30 +0100
Subject: [PATCH 10/12] Recompile documentation

---
 doc/trees.md    | 2 +-
 doc/tutorial.md | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/trees.md b/doc/trees.md
index fbdf29b55..860fad4fa 100644
--- a/doc/trees.md
+++ b/doc/trees.md
@@ -158,7 +158,7 @@ interfaces for such cases:
 It is sometimes useful to have a bidirectional translation between two sorts of trees.
 Inox provides a mechanism to maintain an encoder/decoder pair alongside a pair of
 source and target programs through an instance of
-[ProgramTransformer](/src/main/scala/inox/ast/ProgramEncoder.scala).
+[ProgramTransformer](/src/main/scala/inox/transformers/ProgramTransformer.scala).
 
 ## Providing new semantics
 
diff --git a/doc/tutorial.md b/doc/tutorial.md
index 2f0eb5514..6df856508 100644
--- a/doc/tutorial.md
+++ b/doc/tutorial.md
@@ -25,8 +25,8 @@ import inox.solvers._
 
 The explanation is the following:
 - `inox._` imports [`InoxProgram` and many others](/src/main/scala/inox/package.scala#L19)
-- `inox.trees._` imports the content of the default implementation [`trees`](/src/main/scala/inox/package.scala#L58) extending [`Trees`](/src/main/scala/inox/ast/Trees.scala#L10).
-- `inox.trees.dsl._` imports the [domain-specific-language helpers](/src/main/scala/inox/ast/DSL.scala#L20) to create [`trees`](/src/main/scala/inox/package.scala#L58) expressions.
+- `inox.trees._` imports the content of the default implementation [`trees`](/src/main/scala/inox/package.scala#L53) extending [`Trees`](/src/main/scala/inox/ast/Trees.scala#L10).
+- `inox.trees.dsl._` imports the [domain-specific-language helpers](/src/main/scala/inox/ast/DSL.scala#L20) to create [`trees`](/src/main/scala/inox/package.scala#L53) expressions.
 - `inox.solvers._` imports the [solvers](/src/main/scala/inox/solvers/package.scala#L8).
 
 ## Creating the Symbol Table

From a799b3d06d03205dc21993772a862f3b96862776 Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Fri, 19 Feb 2021 14:16:52 +0100
Subject: [PATCH 11/12] Disable link hygiene in mdoc due to false positives

---
 build.sbt | 1 +
 1 file changed, 1 insertion(+)

diff --git a/build.sbt b/build.sbt
index dc8f64ad2..e4025fc2b 100644
--- a/build.sbt
+++ b/build.sbt
@@ -105,6 +105,7 @@ lazy val genDoc = taskKey[Unit]("Typecheck and interpret the documentation")
 
 mdocIn  := sourceDirectory.value / "main" / "doc"
 mdocOut := baseDirectory.value / "doc"
+mdocExtraArguments := Seq("--no-link-hygiene")
 
 genDoc := { () }
 genDoc := (genDoc dependsOn (compile in Compile)).value

From 03d45dd07a804f4a7e5ba2285882ac2aae6540b9 Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Fri, 19 Feb 2021 16:27:43 +0100
Subject: [PATCH 12/12] Use to-string modifier for mdoc (thanks @samarion)

---
 doc/interpolations.md          | 108 +++++++++------------------------
 src/main/doc/interpolations.md |  38 ++++++------
 2 files changed, 46 insertions(+), 100 deletions(-)

diff --git a/doc/interpolations.md b/doc/interpolations.md
index 754fbacad..62f199ad8 100644
--- a/doc/interpolations.md
+++ b/doc/interpolations.md
@@ -53,21 +53,15 @@ Once imported, it is possible to build Inox types and expressions using a friend
 val tpe = t"Boolean"
 // tpe: Type = Boolean
 val expr = e"1 + 1 == 2"
-// expr: Expr = Equals(
-//   Plus(IntegerLiteral(1), IntegerLiteral(1)),
-//   IntegerLiteral(2)
-// )
+// expr: Expr = 1 + 1 == 2
 ```
 
 It is also possible to embed types and expressions:
 
 ```scala
 e"let x: $tpe = $expr in !x"
-// res0: Expr = Let(
-//   ValDef(x, Boolean, List()),
-//   Equals(Plus(IntegerLiteral(1), IntegerLiteral(1)), IntegerLiteral(2)),
-//   Not(Variable(x, Boolean, List()))
-// )
+// res0: Expr = val x: Boolean = 1 + 1 == 2
+// ¬x
 ```
 
 <a name="syntax"></a>
@@ -81,9 +75,9 @@ e"let x: $tpe = $expr in !x"
 
 ```scala
 e"true"
-// res1: Expr = BooleanLiteral(true)
+// res1: Expr = true
 e"false"
-// res2: Expr = BooleanLiteral(false)
+// res2: Expr = false
 ```
 
 <a name="numeric-literals"></a>
@@ -91,7 +85,7 @@ e"false"
 
 ```scala
 e"1"
-// res3: Expr = IntegerLiteral(1)
+// res3: Expr = 1
 ```
 
 Note that the type of numeric expressions is inferred. In case of ambiguity, `BigInt` is chosen by default.
@@ -105,7 +99,7 @@ It is however possible to annotate the desired type.
 
 ```scala
 e"1 : Int".getType
-// res5: Type = BVType(true, 32)
+// res5: Type = Int
 ```
 
 ```scala
@@ -118,7 +112,7 @@ e"1 : Real".getType
 
 ```scala
 e"3.75"
-// res7: Expr = FractionLiteral(15, 4)
+// res7: Expr = 15/4
 ```
 
 <a name="string-literals"></a>
@@ -126,7 +120,7 @@ e"3.75"
 
 ```scala
 e"'Hello world!'"
-// res8: Expr = StringLiteral("Hello world!")
+// res8: Expr = "Hello world!"
 ```
 
 <a name="character-literals"></a>
@@ -134,7 +128,7 @@ e"'Hello world!'"
 
 ```scala
 e"`a`"
-// res9: Expr = CharLiteral('a')
+// res9: Expr = 'a'
 ```
 
 <a name="arithmetic"></a>
@@ -144,13 +138,7 @@ Arithmetic operators are infix and have there usual associativity and priority.
 
 ```scala
 e"1 + 2 * 5 + 6 - 7 / 17"
-// res10: Expr = Minus(
-//   Plus(
-//     Plus(IntegerLiteral(1), Times(IntegerLiteral(2), IntegerLiteral(5))),
-//     IntegerLiteral(6)
-//   ),
-//   Division(IntegerLiteral(7), IntegerLiteral(17))
-// )
+// res10: Expr = ((1 + 2 * 5) + 6) - 7 / 17
 ```
 
 <a name="conditionals"></a>
@@ -158,11 +146,11 @@ e"1 + 2 * 5 + 6 - 7 / 17"
 
 ```scala
 e"if (1 == 2) 'foo' else 'bar'"
-// res11: Expr = IfExpr(
-//   Equals(IntegerLiteral(1), IntegerLiteral(2)),
-//   StringLiteral("foo"),
-//   StringLiteral("bar")
-// )
+// res11: Expr = if (1 == 2) {
+//   "foo"
+// } else {
+//   "bar"
+// }
 ```
 
 <a name="let-bindings"></a>
@@ -170,11 +158,8 @@ e"if (1 == 2) 'foo' else 'bar'"
 
 ```scala
 e"let word: String = 'World!' in concatenate('Hello ', word)"
-// res12: Expr = Let(
-//   ValDef(word, String, List()),
-//   StringLiteral("World!"),
-//   StringConcat(StringLiteral("Hello "), Variable(word, String, List()))
-// )
+// res12: Expr = val word: String = "World!"
+// "Hello " + word
 ```
 
 <a name="lambda-expressions"></a>
@@ -182,30 +167,21 @@ e"let word: String = 'World!' in concatenate('Hello ', word)"
 
 ```scala
 e"lambda x: BigInt, y: BigInt. x + y"
-// res13: Expr = Lambda(
-//   List(ValDef(x, BigInt, List()), ValDef(y, BigInt, List())),
-//   Plus(Variable(x, BigInt, List()), Variable(y, BigInt, List()))
-// )
+// res13: Expr = (x: BigInt, y: BigInt) => x + y
 ```
 
 It is also possible to use the Unicode `λ` symbol.
 
 ```scala
 e"λx: BigInt, y: BigInt. x + y"
-// res14: Expr = Lambda(
-//   List(ValDef(x, BigInt, List()), ValDef(y, BigInt, List())),
-//   Plus(Variable(x, BigInt, List()), Variable(y, BigInt, List()))
-// )
+// res14: Expr = (x: BigInt, y: BigInt) => x + y
 ```
 
 Type annotations can be omitted for any of the parameters if their type can be inferred.
 
 ```scala
 e"lambda x. x * 0.5"
-// res15: Expr = Lambda(
-//   List(ValDef(x, Real, List())),
-//   Times(Variable(x, Real, List()), FractionLiteral(1, 2))
-// )
+// res15: Expr = (x: Real) => x * 1/2
 ```
 
 <a name="quantifiers"></a>
@@ -216,18 +192,9 @@ e"lambda x. x * 0.5"
 
 ```scala
 e"forall x: Int. x > 0"
-// res16: Expr = Forall(
-//   List(ValDef(x, Int, List())),
-//   GreaterThan(
-//     Variable(x, BVType(true, 32), List()),
-//     BVLiteral(true, BitSet(), 32)
-//   )
-// )
+// res16: Expr = ∀x: Int. (x > 0)
 e"∀x. x || true"
-// res17: Expr = Forall(
-//   List(ValDef(x, Boolean, List())),
-//   Or(List(Variable(x, Boolean, List()), BooleanLiteral(true)))
-// )
+// res17: Expr = ∀x: Boolean. (x || true)
 ```
 
 <a name="existential-quantifiers"></a>
@@ -235,24 +202,9 @@ e"∀x. x || true"
 
 ```scala
 e"exists x: BigInt. x < 0"
-// res18: Expr = Not(
-//   Forall(
-//     List(ValDef(x, BigInt, List())),
-//     Not(LessThan(Variable(x, BigInt, List()), IntegerLiteral(0)))
-//   )
-// )
+// res18: Expr = ¬∀x: BigInt. ¬(x < 0)
 e"∃x, y. x + y == 0"
-// res19: Expr = Not(
-//   Forall(
-//     List(ValDef(x, BigInt, List()), ValDef(y, BigInt, List())),
-//     Not(
-//       Equals(
-//         Plus(Variable(x, BigInt, List()), Variable(y, BigInt, List())),
-//         IntegerLiteral(0)
-//       )
-//     )
-//   )
-// )
+// res19: Expr = ¬∀x: BigInt, y: BigInt. (x + y ≠ 0)
 ```
 
 <a name="choose"></a>
@@ -260,15 +212,9 @@ e"∃x, y. x + y == 0"
 
 ```scala
 e"choose x. x * 3 < 17"
-// res20: Expr = Choose(
-//   ValDef(x, BigInt, List()),
-//   LessThan(
-//     Times(Variable(x, BigInt, List()), IntegerLiteral(3)),
-//     IntegerLiteral(17)
-//   )
-// )
+// res20: Expr = choose((x: BigInt) => x * 3 < 17)
 e"choose x: String. true"
-// res21: Expr = Choose(ValDef(x, String, List()), BooleanLiteral(true))
+// res21: Expr = choose((x: String) => true)
 ```
 
 <a name="primitives"></a>
diff --git a/src/main/doc/interpolations.md b/src/main/doc/interpolations.md
index 905c8bd7f..709812045 100644
--- a/src/main/doc/interpolations.md
+++ b/src/main/doc/interpolations.md
@@ -49,14 +49,14 @@ implicit val symbols: inox.trees.Symbols = inox.trees.NoSymbols
 
 Once imported, it is possible to build Inox types and expressions using a friendlier syntax:
 
-```scala mdoc
+```scala mdoc:to-string
 val tpe = t"Boolean"
 val expr = e"1 + 1 == 2"
 ```
 
 It is also possible to embed types and expressions:
 
-```scala mdoc
+```scala mdoc:to-string
 e"let x: $tpe = $expr in !x"
 ```
 
@@ -69,7 +69,7 @@ e"let x: $tpe = $expr in !x"
 <a name="boolean-literals"></a>
 ### Boolean literals
 
-```scala mdoc
+```scala mdoc:to-string
 e"true"
 e"false"
 ```
@@ -77,44 +77,44 @@ e"false"
 <a name="numeric-literals"></a>
 ### Numeric literal
 
-```scala mdoc
+```scala mdoc:to-string
 e"1"
 ```
 
 Note that the type of numeric expressions is inferred. In case of ambiguity, `BigInt` is chosen by default.
 
-```scala mdoc
+```scala mdoc:to-string
 e"1".getType
 ```
 
 It is however possible to annotate the desired type.
 
-```scala mdoc
+```scala mdoc:to-string
 e"1 : Int".getType
 ```
 
-```scala mdoc
+```scala mdoc:to-string
 e"1 : Real".getType
 ```
 
 <a name="real-literals"></a>
 #### Real literals
 
-```scala mdoc
+```scala mdoc:to-string
 e"3.75"
 ```
 
 <a name="string-literals"></a>
 ### String literals
 
-```scala mdoc
+```scala mdoc:to-string
 e"'Hello world!'"
 ```
 
 <a name="character-literals"></a>
 ### Character literals
 
-```scala mdoc
+```scala mdoc:to-string
 e"`a`"
 ```
 
@@ -123,40 +123,40 @@ e"`a`"
 
 Arithmetic operators are infix and have there usual associativity and priority.
 
-```scala mdoc
+```scala mdoc:to-string
 e"1 + 2 * 5 + 6 - 7 / 17"
 ```
 
 <a name="conditionals"></a>
 ## Conditionals
 
-```scala mdoc
+```scala mdoc:to-string
 e"if (1 == 2) 'foo' else 'bar'"
 ```
 
 <a name="let-bindings"></a>
 ## Let bindings
 
-```scala mdoc
+```scala mdoc:to-string
 e"let word: String = 'World!' in concatenate('Hello ', word)"
 ```
 
 <a name="lambda-expressions"></a>
 ## Lambda expressions
 
-```scala mdoc
+```scala mdoc:to-string
 e"lambda x: BigInt, y: BigInt. x + y"
 ```
 
 It is also possible to use the Unicode `λ` symbol.
 
-```scala mdoc
+```scala mdoc:to-string
 e"λx: BigInt, y: BigInt. x + y"
 ```
 
 Type annotations can be omitted for any of the parameters if their type can be inferred.
 
-```scala mdoc
+```scala mdoc:to-string
 e"lambda x. x * 0.5"
 ```
 
@@ -166,7 +166,7 @@ e"lambda x. x * 0.5"
 <a name="universal-quantifiers"></a>
 ### Universal Quantifier
 
-```scala mdoc
+```scala mdoc:to-string
 e"forall x: Int. x > 0"
 e"∀x. x || true"
 ```
@@ -174,7 +174,7 @@ e"∀x. x || true"
 <a name="existential-quantifiers"></a>
 ### Existential Quantifier
 
-```scala mdoc
+```scala mdoc:to-string
 e"exists x: BigInt. x < 0"
 e"∃x, y. x + y == 0"
 ```
@@ -182,7 +182,7 @@ e"∃x, y. x + y == 0"
 <a name="choose"></a>
 ## Choose
 
-```scala mdoc
+```scala mdoc:to-string
 e"choose x. x * 3 < 17"
 e"choose x: String. true"
 ```