The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

On Wed, Jan 21, 2015 at 8:42 PM, Enrico Tassi 
<enrico.tassi AT inria.fr>
 wrote:
> On Wed, Jan 21, 2015 at 07:32:28PM +0100, Ali Assaf wrote:
>> Hi,
>>
>> The description of Matita's kernel implementation in "A compact kernel
>> for the calculus of inductive constructions" contains a type system in
>> the appendix that includes metavariables, although it is not
>> commented.
>
> That type system is the one for the kernel.  Metavariables are pretty
> much like constants, they have a type declared in a dedicated
> environment and they are only equal to themselves.

This is what I need...

>
> Things get interesting when the conversion test is allowed to
> instantiate them in order to succeed.  In this case is more correct to
> call the conversion test higher order unification.  This algorithm is
> not properly documented in such paper, and not in any other paper about
> Matita.  Eventually it will be...


...since this is what I'm doing ;-)

>
> Best,
> --
> Enrico Tassi