use operators +, -, * provided by class num

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@17136 cec4b9c1-7d33-0410-9eda-942365e851bb
spechub · Aug 7, 2012 · 588e765 · 588e765
1 parent 16557be
commit 588e765
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/Comorphisms/Hs2HOLCFaux.hs b/Comorphisms/Hs2HOLCFaux.hs
@@ -365,7 +365,7 @@ mthFunctor  = ["fmap"]
 mthFractional = ["/","recip","fromRational"]
 mthAll     = mthEq ++ mthOrd ++ mthEnum ++ mthNum
               ++ mthIntegral ++ mthFractional ++ mthBounded
-aweLits     = mthMonad ++ mthFunctor ++ mthEq
+aweLits     = mthMonad ++ mthFunctor ++ mthEq ++ ["+", "-", "*"]
 
 nameListA, nameListB, nameListC, nameListD :: [String]
 nameListE, nameListF, nameListH :: [String]
@@ -423,9 +423,9 @@ trOSym s = case s of
      "<="      -> "leq"
      ">"       -> "more"
      ">="      -> "meq"
-     "+"       -> "add"
-     "*"       -> "prod"
-     "-"       -> "diff"
+     "+"       -> "+"
+     "*"       -> "*"
+     "-"       -> "-"
      "^"       -> "pow"
      "^^"      -> "fpow"
      "++"      -> "bconcat"

diff --git a/Haskell/test/HOL/mrec.hs b/Haskell/test/HOL/mrec.hs
@@ -4,7 +4,7 @@ data Natx a = Zx | Sx a (Natx a)
 fun1 :: Natx Int -> (Natx Int, Int)
 fun1 x = case x of 
        Zx -> (Zx, 0) 
-       Sx n k -> (Sx n (fst (fun1 k)), n * (fun2 k))
+       Sx n k -> (Sx n (fst (fun1 k)), n * (fun2 k) - 0)
 
 fun2 :: Natx Int -> Int 
 fun2 x = case x of