4 ms·
> a proof development system, aka dependently typed programming language. There are proof assistants without dependent types, like Isabelle/HOL.
by creata 5y ago
> a proof development system, aka dependently typed programming language.
There are proof assistants without dependent types, like Isabelle/HOL.