# Pastebin 1KpKMytX
-- I'm trying to write this
strings-are-quoted : (s : List Char) → just (lit (string s)) ≡ parse (display (render-pretty 80 (char '"' <> text s <> char '"')))
strings-are-quoted [] = {!!}
strings-are-quoted (x ∷ xs) = {!!}

-- Hole ?1
--
-- ?1 : just (lit (string [])) ≡
-- parse
-- (display
-- (render-pretty (fromNat 80) (char '\"' <> text [] <> char '\"')))

-- agda-compute-normalised-maybe-toplevel for:

-- parse
-- (display
-- (render-pretty (fromNat 80) (char '\"' <> text [] <> char '\"')))

-- is

-- just (lit (string []))

-- but this doesn't type check:

-- strings-are-quoted : (s : List Char) → just (lit (string s)) ≡ parse (display (render-pretty 80 (char '"' <> text s <> char '"')))
-- strings-are-quoted [] = refl

{-

just (lit (string [])) !=
parse
(display
(render-pretty (fromNat 80) (char '\"' <> text [] <> char '\"')))
of type Maybe Syntax
when checking that the expression refl has type
just (lit (string [])) ≡
parse
(display
(render-pretty (fromNat 80) (char '\"' <> text [] <> char '\"')))

-}