CODEWITHSUNDEEP
coqisabelle
TomR
TomR

Reputation: 3056

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?

Upvotes: 1

Views: 173

Answers (1)

Joachim Breitner
Joachim Breitner

Reputation: 25763

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)

Upvotes: 3

Related Questions