Elegant elaboration with function invocation

05/31/2021

∙

by   Tesla Zhang, et al.

∙

0

∙

share

We present an elegant design of the core language in a dependently-typed lambda calculus with δ-reduction and an elaboration algorithm.