Questions tagged [implicit-argument]

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

Filter by
Sorted by
Tagged with
1 vote
1 answer
49 views

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
65 views

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
126 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....
  • 157
7 votes
1 answer
124 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 ...
  • 671
20 votes
3 answers
379 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. ...
  • 4,740