[Agda] syntactic sugar parameters

[Herminie Pagel]

Hi there,

when following the kripke semantics file of the Iowa Agda Library:
https://github.com/cedille/ial/blob/master/kripke-semantics.agda#L37

we find in L37:
sample-pf = ImpliesI{$ "p"} (AndI (Assume{[]}) (Assume))
which is a proof of type [] ⊢ Implies ($ "p") (And ($ "p") ($ "p"))

i tested
sample-pf-alt = ImpliesI (AndI (Assume{[]} {($ "p")}) (Assume{[]} {($
"p")}))
and results also in a proof of the same type

What kind of syntactic sugar is making agda understand sample-pf without
explicitly telling Assume its parameters in the first place?

best, herminie
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191205/89efda2a/attachment.html>