Questions tagged [implicit-argument]
An implicit argument is an argument which can be inferred from contextual knowledge.
6
questions
9
votes
2
answers
151
views
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
50
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 ...
- 90
3
votes
1
answer
79
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 ...
- 237
6
votes
1
answer
143
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
135
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
407
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. ...
- 5,424