arith.hs

evalBigStep :: Tm -> Maybe Tm
evalBigStep (TmIf t1 t2 t3) = 
    evalBigStep t1 >>= \b1 -> case b1 of
        TmTrue  -> evalBigStep t2                       -- (B-IfTrue)
        TmFalse -> evalBigStep t3                       -- (B-IfFalse)
        _       -> Nothing
evalBigStep (TmSucc t1) =
    evalBigStep t1 >>= \t1' -> case t1' of
        nv1 | isNumerical nv1 -> Just (TmSucc nv1)      -- (B-Succ)
        _                     -> Nothing
evalBigStep (TmPred t1) =
    evalBigStep t1 >>= \t1' -> case t1' of
        TmZero                         -> Just TmZero   -- (B-PredZero)
        (TmSucc nv1) | isNumerical nv1 -> Just nv1      -- (B-PredSucc)
        _                              -> Nothing
evalBigStep (TmIsZero t1) =
    evalBigStep t1 >>= \t1' -> case t1' of
        TmZero     -> Just TmTrue                       -- (B-IsZeroZero)
        (TmSucc _) -> Just TmFalse                      -- (B-IsZeroZero)
        _          -> Nothing
evalBigStep v = Just v