How to have arbitrary observational equations involving java types

[Sinha-Ujjawal]

Hi, I have a requirement where I need observation_equations involving java types. How can I possibly do that?

typeside Ty = literal {
	external_types
		Int -> "java.lang.Integer"
	
	external_parsers
		Int -> "parseInt"

	external_functions
	 	min : Int, Int -> Int = "(x, y) => x < y ? x : y"
}

schema C = literal : Ty {
	entity
		A

	foreign_keys

	path_equations

	attributes
		x : A -> Int
		y : A -> Int

	observation_equations
		forall a. a.x = min(a.x, a.y) # I just want to check a.x < a.y. How can I do that?
}

So in this simplified example, I want to enforce that all instances of schema C should fulfil the constraint that forall a. a.x < a.y. Is there a way to implement this?

[wisnesky]

I'm sorry, I didn't see this ticket until now. What's going on here is a limitation of theorem proving - the equation "x = f(x,y)" is "tricky". But it works if you add "options prover = completion
completion_precedence = "x min y"" to the schema C, everything works.