[Agda] syntactic sugar parameters

[James Wood]

More recently, here is the documentation on the syntactic aspects:
https://agda.readthedocs.io/en/v2.6.0.1/language/implicit-arguments.html
. Unfortunately, it seems not to document how elided terms are inferred,
but as Nils says, the usual way is unification. To get a feel of this,
it might be instructive to delete the body of `sample-pf` and build up
the term yourself. You'll see where the checker can figure things out
and where it can't.

James

On 06/12/2019 09:09, Nils Anders Danielsson wrote:
> On 2019-12-05 13:05, Herminie Pagel wrote:
>> What kind of syntactic sugar is making agda understand sample-pf
>> without explicitly telling Assume its parameters in the first place?
> 
> Agda uses unification to infer these arguments. Ulf Norell's PhD thesis
> discusses this topic (but Agda has evolved quite a bit since the thesis
> was published).
>