leodemoura/lean — pull request #5 by soonhokong (2013-09-29 06:43:55+00:00)
Title: Suggestion for lean_assert

Hi Leo, what do you think about this change?

Here are two examples:

LEAN ASSERTION VIOLATION
File: /Users/soonhok/work/lean/src/tests/util/numerics/mpbq.cpp
Line: 264
root_upper(n9, x9, 3) == false
Arguments
root_upper(n9, x9, 3) : bool := true
false : bool := false

LEAN ASSERTION VIOLATION
File: /Users/soonhok/work/lean/src/tests/util/numerics/mpbq.cpp
Line: 267
n10 == mpbq(1, 0)
Arguments
n10 : lean::mpbq := 3/2
mpbq(1, 0) : lean::mpbq := 1