6

I would find a different tutorial because the author of that one is fundamentally confused. They wrongly claim that $\neg a$ and $\bot\to a$ are equivalent ($a\to\bot$ would be correct), and also wrongly claim that you can't write a function of type $\texttt{Void}\to a$. $\texttt{Void}\to a$ is vacuously true. In principle a function of that type should ...


4

The dependent types allow you to specify what properties your function should have, not just what its domain and codomain are. This way it becomes impossible to accidentally use the wrong function. For example, suppose we want a function that sorts lists (of integers). In ordinary programming we would ask for a value of type List → List, and then we would ...


1

The difference is in what kind of type theorem/Prop is. In Isabelle, theorem is a type in the underlying implementation language, that is made abstract so that the only way to create an inhabitant of that type (i.e. a valid theorem) is in the end to resort to the primitives provided by the kernel. So it is the typing constraints of the implementation ...


Only top voted, non community-wiki answers of a minimum length are eligible