[x] maybe-beta, e.g. in fun x => f x (A x) we detect A x
[x] maybe-eta, e.g. fun x => f (A x) is a maybe-eta (+ A x is a maybe-beta)
[x] maybe-llam, e.g. F a b is a maybe-llam
[x] Goal compilation
[x] maybe-beta, e.g. in fun x => f x (A x) we detect A x
[x] maybe-eta, e.g. fun x => f (A x) is a maybe-eta (+ A x is a maybe-beta)
[x] maybe-llam, e.g. F a b is a maybe-llam
The main difference between instance and goal compilation is that in the instance we work on a closed term.
In the goal, we can have coq unification variables.
fun x => f x (A x)we detectA xfun x => f (A x)is a maybe-eta (+A xis a maybe-beta)F a bis a maybe-llamfun x => f x (A x)we detectA xfun x => f (A x)is a maybe-eta (+A xis a maybe-beta)F a bis a maybe-llamThe main difference between instance and goal compilation is that in the instance we work on a closed term. In the goal, we can have coq unification variables.