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). -- /NAD