Search code examples
coqisabelle

What is Isabelle/HOL command for Compute in Coq?

Proof assistant Coq have compute command (and also check command for determination of the type) which returns the result of function application. Does Isabelle/HOL have similar command and how it is named?

Solution

  • Isabelle has a "value" command that performs evaluation.

    value "rev [1::nat,2,3]"

    Isabelle then responds with:

    "[Suc (Suc (Suc 0)), Suc (Suc 0), Suc 0]"
  :: "nat list"

    (Quoted from https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2007-October/msg00008.html)