All Questions
Tagged with type-checking coq
3
questions
0
votes
0
answers
41
views
Found no matching subterm in goal while it does seem to be there when doing rewrite
I have two places in my code which are very similar. I want to apply rewrite there. In the first place it works fine. In the other not. Why not?
First place (works fine):
...
1
vote
1
answer
97
views
confused about stlc from Programming Language Foundations
I have two related quetions. I made my way to STLC and Typechecking from Programming Lang Foundations, yet I am more or less mentally stuck at the STLC chapter, hence many things related to it are ...
- 71
6
votes
1
answer
157
views
Does Coq's Module and Functor type-check incrementally?
I am trying to search the following questions online but I failed:
When applying a functor (parametrized module), will the contents inside the functor be re-type-checked?
Will Coq's command ...
- 429