Skip to content

Commit

Permalink
compiler: fix isabelle name error messages
Browse files Browse the repository at this point in the history
[skip lemma]
  • Loading branch information
Zilin Chen authored and Zilin Chen committed Nov 12, 2019
1 parent f09740c commit c58cbc0
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions cogent/src/Cogent/Isabelle/IsabelleName.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit c58cbc0

Please sign in to comment.