Skip to main content
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. ...
Reed Mullanix's user avatar
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,...
ionchy's user avatar
  • 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 ...
Matthew McQuaid's user avatar
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 ...
Lawrence Paulson's user avatar
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 ...
Li-yao Xia's user avatar
  • 1,857
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 ...
Andrej Bauer's user avatar
  • 9,593
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. ...
Meven Lennon-Bertrand's user avatar
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 ...
Meven Lennon-Bertrand's user avatar
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 ...
Meven Lennon-Bertrand's user avatar
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 ...
ice1000's user avatar
  • 6,276
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 ...
Ana Borges's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible