From c58cbc0e2ab0620859e51cf32ba66467c78faabc Mon Sep 17 00:00:00 2001 From: Zilin Chen Date: Tue, 12 Nov 2019 15:07:15 +1100 Subject: [PATCH] compiler: fix isabelle name error messages [skip lemma] --- cogent/src/Cogent/Isabelle/IsabelleName.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/cogent/src/Cogent/Isabelle/IsabelleName.hs b/cogent/src/Cogent/Isabelle/IsabelleName.hs index b19d616ab..bf9637a0b 100644 --- a/cogent/src/Cogent/Isabelle/IsabelleName.hs +++ b/cogent/src/Cogent/Isabelle/IsabelleName.hs @@ -35,12 +35,12 @@ newtype IsabelleName = IsabelleName { unIsabelleName :: String } safeName :: IsabelleName -> IsabelleName safeName (IsabelleName nm) = IsabelleName $ case isReserved nm of - True -> error $ "Error: function name '" ++ nm ++ "' is a reserved isabelle name" + True -> error $ "Error: function name `" ++ nm ++ "' is a reserved isabelle name" -- Add debug note False -> case "_" `isPrefixOf` nm of - True -> error $ "Error: function name" ++ nm ++ "' cannot start with underscores" + True -> error $ "Error: function name `" ++ nm ++ "' cannot start with underscores" False -> case "_" `isSuffixOf` nm of - True -> error $ "Error: function name" ++ nm ++ "' cannot end with underscores" + True -> error $ "Error: function name `" ++ nm ++ "' cannot end with underscores" False -> nm isReserved :: String -> Bool