on master help sign in
Merge pull request #1383 from david-christiansen/issue/1337

Generate legal names for infix op lemmas

commit5277735dd64304e4fe855cbe1e6810e74dc9a842 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 14 Jul 2014, 14:12 (12 years ago) parenta430c3e72cddc6
1 file changed+3−1
src/Idris/Parser.hs+3−1
src/Idris/Parser.hs+3−1
@@ -739,7 +739,9 @@ rhs syn n = do lchar '='; expr syn
739739 <|> do reserved "impossible"; return PImpossible
740740 <?> "function right hand side"
741741 where mkN :: Name -> Name
742− mkN (UN x) = sUN (str x++"_lemma_1")
742+ mkN (UN x) = if (tnull x || not (isAlpha (thead x)))
743+ then sUN "infix_op_lemma_1"
744+ else sUN (str x++"_lemma_1")
743745 mkN (NS x n) = NS (mkN x) n
744746 n' :: Name
745747 n' = mkN n