Re: [isabelle] Isabelle functions: Always total, sometimes undefined
Surely the point is that Coq (or rather its underlying calculus, and similar type theories) have an operational semantics. The semantics of higher-order logic is set-theoretic. Therefore higher-order logic has no definitive operational semantics at all. Rather we identify an executable sublanguage.
> On 19 Oct 2017, at 10:30, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> e) Why there is nothing but a quite loose characterization of the
> ÂexecutableÂ sublanguage of Isabelle/HOL.
> It is the sheer complexity of the system itself: The sublanguage is not
> built into the logic, but appears by a elaborate stack of tools:
This archive was generated by a fusion of
Pipermail (Mailman edition) and