Partial vs Total languages

partial_vs_total.md

All these languages are examples of partial languages, i.e. the result of computing the value of an expression e of type T is one of the following:

• the program terminates with a value in the type T.
• the program e does not terminate.
• the program raises an exception (which has been caused by an incomplete definition).

Agda and other languages based on type theory are total languages in the sense that a program e of type T will always terminate with a value in T.