import Int. import Real. print 1/2 eval 4/6 print 3 div 2 variable x : Real variable i : Int variable n : Nat print x + i + 1 + n set::option lean::pp::coercion true print x + i + 1 + n print x * i + x print x - i + x - x >= 0 print x < x print x <= x print x > x