diff --git a/Makefile b/Makefile
index db0681d2b..196ecf1d2 100644
--- a/Makefile
+++ b/Makefile
@@ -49,7 +49,7 @@ export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS
 export SCHEME
 
 
-.PHONY: all idris2-exec testenv testenv-clean support support-clean clean FORCE
+.PHONY: all idris2-exec libdocs testenv testenv-clean support support-clean clean FORCE
 
 all: support ${TARGET} libs
 
@@ -84,6 +84,12 @@ test-lib: contrib
 
 libs : prelude base contrib network test-lib
 
+libdocs:
+	${MAKE} -C libs/prelude docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
+	${MAKE} -C libs/base docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
+	${MAKE} -C libs/contrib docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
+	${MAKE} -C libs/network docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
+
 ${TEST_PREFIX}/${NAME_VERSION} :
 	${MAKE} install-support PREFIX=${TEST_PREFIX}
 	ln -s ${IDRIS2_CURDIR}/libs/prelude/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/prelude-${IDRIS2_VERSION}
diff --git a/Release/CHECKLIST b/Release/CHECKLIST
index 769988c57..94da293b9 100644
--- a/Release/CHECKLIST
+++ b/Release/CHECKLIST
@@ -3,4 +3,5 @@
 [ ] Change version numbers in prelude, base, contrib, network, and test ipkgs
 [ ] Update bootstrap chez and racket
 [ ] Tag on github with version number (in the form vX.Y.Z)
+[ ] make libdocs and upload to idris-lang.org
 [ ] Run release script
diff --git a/libs/base/Makefile b/libs/base/Makefile
index 0a609e3e4..4f6e005fb 100644
--- a/libs/base/Makefile
+++ b/libs/base/Makefile
@@ -4,5 +4,8 @@ all:
 install:
 	${IDRIS2} --install base.ipkg
 
+docs:
+	${IDRIS2} --mkdoc base.ipkg
+
 clean:
 	$(RM) -r build
diff --git a/libs/contrib/Makefile b/libs/contrib/Makefile
index a5ea667b1..0ac414ef0 100644
--- a/libs/contrib/Makefile
+++ b/libs/contrib/Makefile
@@ -4,5 +4,8 @@ all:
 install:
 	${IDRIS2} --install contrib.ipkg
 
+docs:
+	${IDRIS2} --mkdoc contrib.ipkg
+
 clean:
 	$(RM) -r build
diff --git a/libs/network/Makefile b/libs/network/Makefile
index 8a41f50e9..c1d451411 100644
--- a/libs/network/Makefile
+++ b/libs/network/Makefile
@@ -4,5 +4,8 @@ all:
 install:
 	${IDRIS2} --install network.ipkg
 
+docs:
+	${IDRIS2} --mkdoc network.ipkg
+
 clean:
 	$(RM) -r build
diff --git a/libs/prelude/Makefile b/libs/prelude/Makefile
index 63480597f..0161882bf 100644
--- a/libs/prelude/Makefile
+++ b/libs/prelude/Makefile
@@ -4,5 +4,8 @@ all:
 install:
 	${IDRIS2} --install prelude.ipkg
 
+docs:
+	${IDRIS2} --mkdoc prelude.ipkg
+
 clean:
 	$(RM) -r build
diff --git a/tests/codegen/con001/expected b/tests/codegen/con001/expected
index 1826ce92c..c01e33fa6 100644
--- a/tests/codegen/con001/expected
+++ b/tests/codegen/con001/expected
@@ -16,9 +16,10 @@ prim__gt_Int = [{arg:N}, {arg:N}]: (>Int [!{arg:N}, !{arg:N}])
 prim__believe_me = [{arg:N}, {arg:N}, {arg:N}]: (believe_me [!{arg:N}, !{arg:N}, !{arg:N}])
 prim__crash = [{arg:N}, {arg:N}]: (crash [!{arg:N}, !{arg:N}])
 prim__cast_IntegerInt = [{arg:N}]: (cast-Integer-Int [!{arg:N}])
-Main.main = [{ext:N}]: (Prelude.Interfaces.sum [___, ___, (%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [___, ___, !func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [___, ___, !func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [___, !{arg:N}])))]), (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [___, (%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
+Main.main = [{ext:N}]: (Prelude.Interfaces.sum [___, ___, (%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [___, ___, !func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [___, ___, !func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [___, !{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [___, ___, ___, !{i_con:N}, !funcM, !init, !input]))))))))]), (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [___, (%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
 Prelude.Basics.not = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1), (%constcase 1 0)] Nothing)
 Prelude.Basics.intToBool = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1)] Just 0)
+Prelude.Basics.flip = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: ((!{arg:N} [!{arg:N}]) [!{arg:N}])
 Prelude.Basics.True = Constructor tag Just 0 arity 0
 Prelude.Basics.False = Constructor tag Just 1 arity 0
 Prelude.Basics.Bool = Constructor tag Nothing arity 0
@@ -45,9 +46,10 @@ Prelude.Types.rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (
 Prelude.Types.null = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] (%delay Lazy 0)), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (%delay Lazy 1))] Nothing)
 Prelude.Types.foldr = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] ((!{arg:N} [!{e:N}]) [(Prelude.Types.foldr [___, ___, !{arg:N}, !{arg:N}, !{e:N}])]))] Nothing)
 Prelude.Types.foldl = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (Prelude.Types.foldl [___, ___, !{arg:N}, ((!{arg:N} [!{arg:N}]) [!{e:N}]), !{e:N}]))] Nothing)
+Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.foldl [___, ___, (%lam ma (%lam b (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!ma]) [(%lam {eta:N} (Prelude.Basics.flip [___, ___, ___, !{arg:N}, !b, !{eta:N}]))]))] Nothing))), (%case (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{arg:N}]))] Nothing), !{ext:N}])
 Prelude.Types.Range at Prelude/Types.idr:L:C--L:C = Constructor tag Just 0 arity 4
 Prelude.Types.Range implementation at Prelude/Types.idr:L:C--L:C = [{arg:N}, {arg:N}]: (%con Prelude.Types.Range at Prelude/Types.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromTo [___, !{arg:N}, !{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromThenTo [___, !{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}])))), (%lam {arg:N} (Prelude.Types.rangeFrom [___, !{arg:N}, !{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromThen [___, !{arg:N}, !{arg:N}, !{arg:N}])))])
-Prelude.Types.Foldable implementation at Prelude/Types.idr:L:C--L:C = []: (%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [___, ___, !func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [___, ___, !func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [___, !{arg:N}])))])
+Prelude.Types.Foldable implementation at Prelude/Types.idr:L:C--L:C = []: (%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [___, ___, !func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [___, ___, !func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [___, !{arg:N}]))), (%lam elem (%lam acc (%lam m (%lam {i_con:N} (%lam funcM (%lam init (%lam input (Prelude.Types.foldlM [___, ___, ___, !{i_con:N}, !funcM, !init, !input]))))))))])
 Prelude.Types.takeUntil = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeUntil [___, !{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
 Prelude.Types.takeBefore = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeBefore [___, !{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
 Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Types.Range at Prelude/Types.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
@@ -104,12 +106,14 @@ Prelude.EqOrd.== = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%conc
 Prelude.EqOrd.<= = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
 Prelude.EqOrd.< = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
 Prelude.Interfaces.Functor at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 2 (newtype by 1)
-Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
+Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 4
 Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
-Prelude.Interfaces.sum = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%case (Builtin.fst [___, ___, !{arg:N}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {clam:N} (%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{clam:N}]))] Nothing)))]) [(%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
+Prelude.Interfaces.Constraint (Applicative m) = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing)
+Prelude.Interfaces.sum = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%case (Builtin.fst [___, ___, !{arg:N}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {clam:N} (%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{clam:N}]))] Nothing)))]) [(%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
 Prelude.Interfaces.pure = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{ext:N}]))] Nothing)
-Prelude.Interfaces.foldr = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
-Prelude.Interfaces.foldl = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
+Prelude.Interfaces.foldr = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
+Prelude.Interfaces.foldl = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
+Prelude.Interfaces.>>= = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Monad at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]))] Nothing)
 PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, ___, !{arg:N}])
 PrimIO.case block in case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (!{arg:N} [!{arg:N}])
 PrimIO.case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.case block in case block in io_bind [___, ___, ___, ___, ___, !{arg:N}, ___, (!{arg:N} [!{arg:N}])])
diff --git a/tests/idris2/coverage015/expected b/tests/idris2/coverage015/expected
index 76d4b644e..72a063343 100644
--- a/tests/idris2/coverage015/expected
+++ b/tests/idris2/coverage015/expected
@@ -1,11 +1,11 @@
 1/1: Building Issue1169 (Issue1169.idr)
-LOG coverage.missing:50: Getting constructors for: $resolved1928 [2 closures]
+LOG coverage.missing:50: Getting constructors for: $resolved1964 [2 closures]
 LOG coverage.missing:20: Getting constructors for: (Builtin.Pair String Builtin.Unit)
 LOG coverage.missing:50: Looking for missing alts at type String
-LOG coverage.missing:50: Getting constructors for: $resolved1925 [0 closures]
+LOG coverage.missing:50: Getting constructors for: $resolved1961 [0 closures]
 LOG coverage.missing:20: Getting constructors for: Builtin.Unit
 LOG coverage.missing:20: (Builtin.MkPair {e:0} {e:1} {e:2} {e:3})
-LOG coverage.empty:10: Checking type: TyCon 100 0 params: [] constructors: [$resolved1929] mutual with: [] detaggable by: Just []
+LOG coverage.empty:10: Checking type: TyCon 100 0 params: [] constructors: [$resolved1965] mutual with: [] detaggable by: Just []
 LOG coverage:5: Checking coverage for: (Main.test (Builtin.MkPair String Builtin.Unit {_:368} {_:369}))
 LOG coverage:10: (raw term: (Main.test (Builtin.MkPair String Builtin.Unit {_:368} {_:369})))
 LOG coverage:5: Erased to: (Main.test (Builtin.MkPair [__] [__] {_:368} {_:369}))
diff --git a/tests/idris2/lazy002/expected b/tests/idris2/lazy002/expected
index b91bf12ef..69a30b52e 100644
--- a/tests/idris2/lazy002/expected
+++ b/tests/idris2/lazy002/expected
@@ -1,15 +1,15 @@
-gen 0
-gen 1
-gen 2
-gen 3
-gen 4
-Nothing
-gen 0
-gen 1
-gen 2
-gen 3
-gen 4
-Nothing
 1/1: Building LazyFoldlM (LazyFoldlM.idr)
-LazyFoldlM> LazyFoldlM> LazyFoldlM> 
+LazyFoldlM> gen 0
+gen 1
+gen 2
+gen 3
+gen 4
+Nothing
+LazyFoldlM> gen 0
+gen 1
+gen 2
+gen 3
+gen 4
+Nothing
+LazyFoldlM> 
 Bye for now!