Apostolis Xekoukoulotakis

2018-01-11 09:03:27 UTC

Currently, instance resolution tries all possible ways to construct an

instance argument.

It will look for arguments in the environment and it will use instance

functions to create new ones. If there are multiple solutions, instance

resolution will fail.

example :

Assuming we have defined "less than" as instance.

if we have in the context, a variable q with type zero â€ (suc zero) ,

instance resolution will fail because there are two solutions, q and zâ€n.

But q is in fact zâ€n.

We can prove that there is only one possible construction of the type, thus

any variables with the same type are the same.

At the moment, I am trying to prune my context but it would be nice if

instance resolution was a bit smarter.

instance argument.

It will look for arguments in the environment and it will use instance

functions to create new ones. If there are multiple solutions, instance

resolution will fail.

example :

Assuming we have defined "less than" as instance.

if we have in the context, a variable q with type zero â€ (suc zero) ,

instance resolution will fail because there are two solutions, q and zâ€n.

But q is in fact zâ€n.

We can prove that there is only one possible construction of the type, thus

any variables with the same type are the same.

At the moment, I am trying to prune my context but it would be nice if

instance resolution was a bit smarter.