Rosetta Code

Proof/Haskell: Difference between revisions

Page Discussion

Proof/Haskell (view source)

Revision as of 20:55, 18 February 2010

27 bytes added ,  14 years ago
no edit summary
(I am a math major, hear me roar.)
 
No edit summary
 
Line 88:
subst :: IntExpr -> Equals -> Proof IntExpr
{- A convenience function used internally. -}
subst a (a' :== b) = if| a == a' = return b
else | otherwise = failf2 "subst: %s not the same as %s" a a'▼
then return b
▲ else failf2 "subst: %s not the same as %s" a a'
 
{- All the remaining functions are rules of inference, which allow
Line 108 ⟶ 107:
{- If a = A, b = B, ..., z = Z,
then a + b + ... + z = A + B + ... + Z. -}
equalTerms sum@(Sum l) eqs = do
unless| (length l == length eqs = zipWithM subst l eqs >>= return . (sum :==) $. Sum
| otherwise = failf2 "equalTerms: %s and %s have different lengths" l eqs
zipWithM subst l eqs >>= return . (sum :==) . Sum
 
containsFactor :: IntExpr -> IntExpr -> Proof Divides
{- If p == a*b,
then a | p. -}
expr@(Product l) `containsFactor` x = if x `elem` l
then| x `elem` l = return $ x :| expr
else| otherwise = failf2 "containsFactor: %s not found in %s" x expr
y `containsFactor` _ = failf "containsFactor: %s not a product" y
 
Anonymous user
Retrieved from "https://rosettacode.org/wiki/Special:MobileDiff/139793"