Stream: Coq users

Topic: Atomic tactic and the Ltac language

view this post on Zulip liao zhang (Jul 08 2020 at 07:11):

Hi, sorry to trouble you. According to the documentation, tactics are built from atomic tactics and tactic expressions(like the Ltac language). The are several languages for tactic expressions, like Ltac1, Ltac2... But what is the language for atomic? Ltac1?

view this post on Zulip Karl Palmskog (Jul 08 2020 at 14:42):

I think the manual refers to that certain tactics are implemented directly in OCaml, like auto in tactics/ If this is the case, the tactic is "atomic".

view this post on Zulip Emilio Jesús Gallego Arias (Jul 08 2020 at 14:42):

May be a bit more subtle, if you look at the definition of the tacexpr type

Last updated: Jan 29 2023 at 01:02 UTC