Questions tagged [unification]
Unification is a technique used in the implementation of proof assistants for purposes including solving of metavariables and resolution of type classes.
6
questions
3
votes
1
answer
43
views
Coq: Unify with a pattern and get the result
I want to do change t with (f _), where t is a term and f is a function, but ...
- 71
1
vote
2
answers
132
views
Destruction of unification problem on application
Suppose I have a unification problem
a b = f u
Where f is neutral and u is WHNF and ...
- 5,857
5
votes
0
answers
109
views
Can we bring unification results under cofibrations outside?
Say we have an elaborator which supports metavariables and solve them on flex-rigid cases (with the obvious occurrence checking and scope checking). If we do such unification under a cofibration, do ...
- 5,857
6
votes
0
answers
72
views
What are Generic Arguments in Coq and how are they structured in their OCaml code?
I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
- 199
3
votes
0
answers
63
views
SSReflect tuple constructor: why not use phantom?
I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6....
- 31
7
votes
1
answer
114
views
Tactic unification vs evarconv in Coq
I gather, from practical experience and Zulip hearsay, that Coq has two unification algorithms, known as “tactic unification” and “evarconv”. However, I can't find any documentation on these from a ...
- 758