smalltt

smalltt copied to clipboard

Suspicious slow-down when introducing a meta-variable

2

In the current Agda Implementor's Meeting, we are trying to ~steal~find ideas in `smalltt` to improve Agda's performance. In the process of doing so, in the context of deciding whether...

omelkonian

Hello. I've recently managed to implement a proper NbE on [HVM](https://github.com/Kindelia/HVM/blob/master/examples/normalization-by-evaluation.hvm), an optimal λ-calculus evaluator. By proper, I mean that any term that is reducible by HVM will be reducible...

VictorTaelin

Suppose, for example, we want to type-check the following term: ``` main : ∀(b: Bool) -> (if b then Nat else Char) = λb -> (match b { true: ;...

VictorTaelin