definitions: missing check and AssertionError

[erniecohen]

The manual says that definitions are equivalent to axioms. However, the following verifies, and when the definition is changed to an axiom, it gets a syntax error for assigning to a function used in an axiom:

function f(T:bool) : bool definition f(T:bool) = T after init { f(T) := false; }
I assume that definitions should give the same error.

Moreover, if you add an assertion at the end of the initializer above, ivy_check gets an AssertionError.