Skip to main content

Questions tagged [total]

A total function is defined on all inputs and always terminates. Contrast with partial functions.

Filter by
Sorted by
Tagged with
18 votes
1 answer
306 views

How can all functions be total in Isabelle?

Isabelle/HOL’s logic is called a logic of “total functions”, yet there are functions that are obviously not total, such as division div. How does this make sense?
Joachim Breitner's user avatar