diff --git a/experiments/idris/src/Fathom/Closed/IndexedInductive.idr b/experiments/idris/src/Fathom/Closed/IndexedInductive.idr
index abec1a96e..5d2e11de3 100644
--- a/experiments/idris/src/Fathom/Closed/IndexedInductive.idr
+++ b/experiments/idris/src/Fathom/Closed/IndexedInductive.idr
@@ -68,10 +68,10 @@ namespace FormatOf
 
   export
   encode : {0 A, S : Type} -> (f : FormatOf A) -> Encode A (Colist S)
-  encode End () = Just []
-  encode (Pure x) (MkSing _) = Just []
+  encode End () = pure []
+  encode (Pure x) (MkSing _) = pure []
   encode (Ignore f def) () = encode f def
-  encode (Repeat Z f) [] = Just []
+  encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]
   encode (Bind f1 f2) (x ** y) =
diff --git a/experiments/idris/src/Fathom/Closed/IndexedInductiveCustom.idr b/experiments/idris/src/Fathom/Closed/IndexedInductiveCustom.idr
index d1754ba3b..3def39cf7 100644
--- a/experiments/idris/src/Fathom/Closed/IndexedInductiveCustom.idr
+++ b/experiments/idris/src/Fathom/Closed/IndexedInductiveCustom.idr
@@ -83,10 +83,10 @@ namespace FormatOf
 
   export
   encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream
-  encode End () = Just []
-  encode (Pure x) (MkSing _) = Just []
+  encode End () = pure []
+  encode (Pure x) (MkSing _) = pure []
   encode (Ignore f def) () = encode f def
-  encode (Repeat Z f) [] = Just []
+  encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]
   encode (Bind f1 f2) (x ** y) =
diff --git a/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr b/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr
index 040d515bd..61ab87165 100644
--- a/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr
+++ b/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr
@@ -100,13 +100,13 @@ namespace Format
 
   export
   encode : (f : Format) -> Encode (Rep f) (Colist a)
-  encode End () = Just []
-  encode (Pure x) (MkSing _) = Just []
+  encode End () = pure []
+  encode (Pure x) (MkSing _) = pure []
   encode (Ignore f def) () = encode f def
-  encode (Repeat Z f) [] = Just []
-  encode (Repeat (S len) f) (x :: xs) = do
+  encode (Repeat Z f) [] = pure []
+  encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]
-  encode (Bind f1 f2) (x ** y) = do
+  encode (Bind f1 f2) (x ** y) =
     [| encode f1 x <+> encode (f2 x) y |]
 
 
diff --git a/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr b/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr
index 3a3e9d617..7aee799b7 100644
--- a/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr
+++ b/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr
@@ -97,10 +97,10 @@ namespace Format
 
   export
   encode : (f : Format) -> Encode (Rep f) ByteStream
-  encode End () = Just []
-  encode (Pure x) (MkSing _) = Just []
+  encode End () = pure []
+  encode (Pure x) (MkSing _) = pure []
   encode (Ignore f def) () = encode f def
-  encode (Repeat Z f) [] = Just []
+  encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]
   encode (Bind f1 f2) (x ** y) =
diff --git a/experiments/idris/src/Fathom/Open/Record.idr b/experiments/idris/src/Fathom/Open/Record.idr
index 888dd4c57..61cdfff0c 100644
--- a/experiments/idris/src/Fathom/Open/Record.idr
+++ b/experiments/idris/src/Fathom/Open/Record.idr
@@ -72,7 +72,7 @@ namespace Format
     decode = pure (MkSing x)
 
     encode : Encode Rep ByteStream
-    encode (MkSing _) = Just []
+    encode (MkSing _) = pure []
 
 
   public export
@@ -106,7 +106,7 @@ namespace Format
     encode : Encode Rep ByteStream
     encode = go len where
       go : (len : Nat) -> Encode (Vect len f.Rep) ByteStream
-      go 0 [] = Just []
+      go 0 [] = pure []
       go (S len) (x :: xs) =
         [| f.encode x <+> go len xs |]