NOTE: application transformation of function with implicit

Recently, I'm working on a theorem prover, and implementing implicit parameters. This brings a hard problem for me, and the idea get from type theory elaboration implementation should be recorded for myself! So here is the idea, the following definition is classic equality, type part.

(def (= {A : Type}
	[a b : A])
  : Type

In my theorem prover, one can write

(= T t t)
# or
(= t t)

It's clear that the second one is the point and usually we write down. So how to type check it? The idea is generating a fresh meta for it:

(= ?T t t)

Then unification should work!

Date: <2022-04-06 Wed> Wed Apr 6 02:32:40 UTC 2022

Author: Lîm Tsú-thuàn