Questions tagged [type-checking]
Checking that types adhere to the tying rules.
7
questions
2
votes
1
answer
82
views
Why does an internal term produced by Lean's equation compiler have holes in it?
Section 4.7 of the Lean reference manual (version 3.3) gives an example of a division function defined by well-founded recursion. I used the #print command to ...
- 35
1
vote
1
answer
65
views
Code obtained from printing a definition from the Lean 3.46 equation compiler does not type check. Why doesn't it, and how can I fix it?
In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running ...
- 35
6
votes
1
answer
258
views
How do I convince the Lean 4 type checker that addition is commutative?
In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the ...
- 63
6
votes
1
answer
113
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
16
votes
2
answers
2k
views
What is bidirectional type checking?
What is bidirectional type checking and why would I want to implement it?
It feels like the name is a bit of a misnomer and the syntactic separation kind of resembles stuff like ANF, call by push ...
- 2,648
9
votes
1
answer
265
views
Type Checking Undecidable in Extensional Type Theory
What is the difference between intensional vs extensional type theories and how come the type checking is undecidable for extensional type theory? Also, how does it affect the expressiveness of ...
- 248
11
votes
1
answer
165
views
In the "Simply Easy!" paper, why is it safe to evaluate types in the empty environment?
The paper in question: An Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and Wouter Swierstra.
I'm wondering whether it's correct in what's it is doing. Precisely ...
- 671