Questions tagged [implicit-argument]

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

Filter by
Sorted by
Tagged with
9 votes
2 answers

Uses of first-class implicit function types

Many proof assistants have a way to make certain arguments of a function as "implicit", so that the user doesn't have to supply them but they will be solved by unification. Sometimes, such ...
  • 2,832
1 vote
1 answer

Non-dependent implicit argument instantiation in Coq's reference manual does not work

Consider the following definition Definition foo1 (A : Type) {_ : A} := A. I was wondering whether there is a way to instantiate the non-dependent implicit ...
3 votes
1 answer

Can I specify `refl`'s parameter explicitly in Agda?

I'm working on some proofs in Agda that, for educational purposes, explicitly use the path induction principle (which I've defined myself) rather than pattern matching. In the theoretical mathematical ...
6 votes
1 answer

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....
  • 157
7 votes
1 answer

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 ...
  • 671
20 votes
3 answers

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. ...
  • 5,424