14
votes
Accepted
Are implicit arguments essential to (dependently-typed) proof assistants?
I would argue no, they are only necessary for reducing the suffering caused by other issues. In particular, one of the largest reasons we need implicits are various issues caused by bundling problems.
...
- 156
10
votes
Are implicit arguments essential to (dependently-typed) proof assistants?
The only proof assistant I know of that doesn't have the usual notion of implicit arguments is Cedille. However:
It is a CC without a universe hierarchy and has syntactic stratification between terms,...
- 1,026
6
votes
Accepted
Can I specify `refl`'s parameter explicitly in Agda?
You absolutely can. Given the default definition of the identity type
data _β‘_ {a} {A : Set a} (x : A) : A β Set a where
refl : x β‘ x
we have that
...
- 376
5
votes
Uses of first-class implicit function types
Here is a small and concrete example that I think looks better thanks to Agda's strategy. First, let me show what's wrong in Coq. Consider this type of natural transformations of functors ...
- 2,242
5
votes
Accepted
How to recover implicit arguments of inductive types in a match expression?
In Lean @foo is like foo but with all arguments made explicit, see documentation on implicit arguments (search for ...
- 11k
5
votes
Are implicit arguments essential to (dependently-typed) proof assistants?
This question presumes that proof assistants necessarily support dependent type theories. There is no use for implicit arguments in proof assistants based on simple type theory, such as Isabelle or ...
- 816
4
votes
Accepted
Strict implicit arguments in Coq
The type of s is forall g, arrows g -> obj g. You can't infer g from ...
- 2,242
3
votes
Accepted
How to set defaults for implicit arguments when they can't be inferred?
Not sure how robust that is, but you can do something quite nice using typeclasses.
...
- 5,928
2
votes
Implementation details of implicit arguments
I donβt think there is any detailed paper description of this for Coq, however there is one for Matita which as far as I know is quite close to how Coq does things.
Unification is taken as a black box ...
- 5,928
2
votes
In Coq, are there drawbacks in making implicit some arguments?
One potential reason is partial application: if you often want to apply eq_ind to all its arguments except the proof of equality (getting something of type ...
- 5,928
2
votes
Type inference with type classes in Coq
The way to use type classes is to think of them as additional structure on original structure, and not a larger structure that contains the original one.
Let's explain this with a simple example first....
- 11k
1
vote
Type inference with type classes in Coq
If you want to use π to mean cat_Bin_from_FP π, the relevant feature is coercions, not type classes.
...
- 2,242
1
vote
Why doesn't the proof found by Agda's automatic search (with dot-prefixed patterns) work?
Dotted patterns are also known as inaccessible patterns. My understanding is that the matched bindings are inaccessible, because they are generated from index unification. That's why they are marked ...
- 6,532
1
vote
Accepted
Non-dependent implicit argument instantiation in Coq's reference manual does not work
This is probably a Coq version mismatch. The default online reference manual is for the most recent Coq, which is 8.15.2 at the time of writing. In this version it works. I just tested 8.12.2 and I ...
- 946
Only top scored, non community-wiki answers of a minimum length are eligible