We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 39ae011 commit 4755bccCopy full SHA for 4755bcc
slides/.gitignore
@@ -1,6 +1,8 @@
1
# Unless you want to add it manually
2
3
main.pdf
4
+result
5
+result/
6
7
### LaTeX ###
8
## Core latex/pdflatex auxiliary files:
slides/main.md
@@ -107,11 +107,10 @@ f k _ t (succ zero)
107
```
108
109
* replace `_` with `?¹`
110
+* look up `k` yields not fully elaborated term *yet*
111
* you get a constraint `?¹ ~ F ?²`
112
* looking up `t` yields type `G`
113
* produce a constraint `F ?² ~ G`
-* look up `k` yields not fully elaborated term *yet*
114
-* can't solve it for now, so just stash it and hope we can solve it later
115
116
## How do constraints work
117
0 commit comments