Elegant elaboration with function invocation
arXiv:2105.14840
Abstract
We present an elegant design of the core language in a dependently-typed lambda calculus with -reduction and an elaboration algorithm.
arXiv comment6 pages, 3 figures
arXiv:2105.14840
We present an elegant design of the core language in a dependently-typed lambda calculus with -reduction and an elaboration algorithm.
arXiv comment6 pages, 3 figures