ImplicitArg

See the official user manual for the most up-to-date version of the information on this page.

The implicit argument feature of Agda is only a syntactic facility (no change in the type theory). This uses the notion of metavariables. One can declare type schemas following the following BNF (due to Conor McBride)

  Sch ::= Ty | (x : Sch) -> Sch | {x : Ty} -> Sch

  ren : {Γ Δ : Ctx} (r : {τ : Ty} -> Var Γ τ -> Var Δ τ)
      -> {τ : Ty} -> Tm Γ τ -> Tm Δ τ
  ren = ?
  id_ren = ren (\x -> x)

The scheme outlined above has been proposed, but not implemented. Implicit arguments are currently handled in a different way.

Using this syntax the user tells to the system where to insert meta-variables. The intention is then that these meta-variables can be found from the constraints produced by type-checking.