Questions tagged [implicit-argument]

An implicit argument is an argument which can be inferred from contextual knowledge.

Filter by
Sorted by
Tagged with
6 votes
1 answer
102 views

How to set defaults for implicit arguments when they can't be inferred?

If I had a module declared as follows in file A.v: Section A. Context {𝒳 : Set}. Inductive abt := Abt_leaf (x : 𝒳) | Abt_node. End A. And in another file, B....
user avatar
  • 157
6 votes
1 answer
118 views

Implementation details of implicit arguments

How do the implicit arguments work in proof assistants such as Agda or Coq? Specifically, how are the blanks filled in? What kind of resolution algorithm is used? Are there any papers written about ...
user avatar
  • 651
20 votes
3 answers
361 views

Are implicit arguments essential to (dependently-typed) proof assistants?

Inspired from the roundtable discussion held by Richard Eisenburg in WITS, I'm wondering if implicit arguments are really necessary for proof assistants? Right now, they generate a lot of problems. ...
user avatar
  • 4,136