-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
91 changed files
with
14 additions
and
3,049 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,20 +1,15 @@ | ||
将 explicit-substitution 从 lambda 中分离出来 | ||
rename lang1 to lang | ||
|
||
# 有待验证的假设 | ||
> 在 explicit-substitution 中实验,然后开始 cicada。 | ||
在 explicit-substitution 中实验,然后开始 cicada。 | ||
支持 `(assert-equal)` 与 `(assert-not-equal)` | ||
|
||
- 用 `assert-equal` 验证基于 `Exp` 的 definitional 等价关系。 | ||
- 验证基于 `Exp` 的递归函数之间的 definitional 等价关系。 | ||
- 验证基于 `Exp` 的 dependent type 类型检查器。 | ||
- 在实现 explicit-substitution 时避免全局的 `globalFreshen`。 | ||
|
||
# lang1 | ||
支持直接递归函数与相互递归函数,不能判断等价的地方就不判断。 | ||
|
||
[lang1] 支持 `(assert-equal)` 与 `(assert-not-equal)` | ||
[lang1] 支持直接递归函数与相互递归函数,不能判断等价的地方就不判断。 | ||
- 验证基于 `Exp` 的递归函数之间的 definitional 等价关系。 | ||
|
||
# lang0 | ||
验证基于 `Exp` 的 dependent type 类型检查器。 | ||
|
||
[lang0] docs/lambda-encoding -- Exp Lambda 编码的例子,外加解释器 | ||
[lang0] docs/self-type | ||
在实现 explicit-substitution 时避免全局的 `globalFreshen`。 |
File renamed without changes.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.