All Questions
Tagged with type-checking dependent-type
5
questions
3
votes
1
answer
84
views
How to read/understand the definition of the environment in type-checking?
I am trying to read the code for TinyIdris, but couldn't understand one of the first definitions about environments below (because of my lack of understanding about type-checking and/or dependent ...
- 2,220
5
votes
2
answers
226
views
What is a context mapping in dependent type checking?
I am reading a dissertation about dependent type programming language (Norell, 2007), and had much trouble understanding the definition of context mappings/substitutions as shown in the figure below .
...
- 2,220
7
votes
1
answer
619
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 ...
- 73
10
votes
1
answer
467
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 ...
- 258
11
votes
1
answer
183
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 ...
- 731