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.