Various cleanups

Author: brendanzab

experiments/idris/src/Fathom/Closed/IndexedInductive.idr

@@ -82,6 +82,7 @@ encode (Bind f1 f2) (x ** y) =
 -----------------
 
 
+public export
 record Format where
   constructor MkFormat
   0 Repr : Type

experiments/idris/src/Fathom/Closed/InductiveRecursive.idr

@@ -114,18 +114,6 @@ decode (Bind f1 f2) buffer = do
   (y, buffer'') <- decode (f2 x) buffer'
   Just ((x ** y), buffer'')
 
--- Questionable format descriptions
--- decode (OrPure True f _) buffer = decode f buffer
--- decode (OrPure False _ def) buffer = Just (def, buffer)
--- decode (OfSing f (MkSing r {prf})) buffer = do
---   (x, buffer') <- decode f buffer
---   Just (rewrite sym prf in x, buffer')
--- decode (OfEq f _ {prf}) buffer = do
---   (x, buffer') <- decode f buffer
---   Just (rewrite sym prf in x, buffer')
-
--- Broken stuff
-
 
 export
 encode : (f : Format) -> Encode (Rep f) (Colist a)
@@ -137,14 +125,6 @@ encode (Repeat (S len) f) (x :: xs) = do
   [| encode f x <+> encode (Repeat len f) xs |]
 encode (Bind f1 f2) (x ** y) = do
   [| encode f1 x <+> encode (f2 x) y |]
--- Questionable format descriptions
--- encode (OrPure True f _) x = encode f x
--- encode (OrPure False _ def) x = Just []
--- encode (OfSing f r) x = do
---   buffer' <- encode f ?todo_x
---   ?todo_encode
--- encode (OfEq f _ {prf}) x = do
---   encode f (rewrite prf in x)
 
 
 -----------------

experiments/idris/src/Playground.idr

@@ -84,9 +84,4 @@ indexedToIndRec (Repeat len f) with (indexedToIndRec f)
   indexedToIndRec (Repeat len _) | MkFormatOf f = MkFormatOf (IndRec.Repeat len f)
 indexedToIndRec (Bind f1 f2) with (indexedToIndRec f1)
   indexedToIndRec (Bind _ f2) | MkFormatOf f1 =
-    --    f1 : Format
-    --  0 A : Type
-    --    f2 : (x : Rep f1) -> FormatOf (B x)
-    -- ------------------------------
-    -- todo_indexedToIndRec : FormatOf (DPair (Rep f1) (\x => B x))
     ?todo_indexedToIndRec