A dependently-typed Agda taster - Part II by Matthew Brecknell (@mbrcknl)
A dependently-typed Agda taster - Part II
By Matthew Brecknell (@mbrcknl)
We'll show how to build evidence that a certain thing can be found in a list, and how to use this evidence to safely retrieve a different thing from some other suitably-indexed heterogeneous list.
Finally, if we have time, we'll use what we just built to embed the simply-typed lambda calculus.