Stream: Beginner Questions

Topic: Why does "TERM _" appear.

view this post on Zulip irvin (Jun 09 2025 at 13:41):

I was playing around with PRIMITIVE and I've noticed that if I do

ML‹
val print_internal_goal = PRIMITIVE (fn x => (@{print} x ; x))
›
lemma "a ⟹ (b ⟹ a)" "b"
  apply (tactic print_internal_goal)

I get the following printed

"TERM _"⌂
"(a ⟹ b ⟹ a) ⟹ b ⟹ ((a ⟹ b ⟹ a) &&& b)"⌂

What is the origin of the "TERM _"

view this post on Zulip Kevin Kappelmann (Jun 11 2025 at 06:57):

as far as i know, it is used to check whether your tactic fails gracefully (i.e. return an empty sequence) in case it is applied to a state that it cannot act on. See #Archive Mirror: Isabelle Users Mailing List > [isabelle] emergence of "TERM _" (using quickcheck and ni... @ 💬

view this post on Zulip irvin (Jun 12 2025 at 01:11):

Thanks!

view this post on Zulip Manuel Eberl (Jun 13 2025 at 17:32):

Note that you probably should not use PRIMITIVE etc directly. Whatever you want to do can probably also be done with high level combinators like Subgoal.FOCUS

Last updated: Jun 21 2025 at 01:46 UTC