7.12 Developing certified program
This section is devoted to powerful tools that Coq provides to develop certified programs. We just mention below the main features of those tools and refer the reader to chapter 18 and references [79, 80] for more details and examples.7.12.1 Realizer term
This command associates the term term to the current goal. The term's syntax is described in the chapter 18. It is an extension of the basic syntax for Coq's terms. The Realizer is used as a hint by the Program tactic described below. The term term intends to be the program extracted from the proof we want to develop.See also: chapter 18, section 15.1
7.12.2 Program
This tactic tries to make a one step inference according to the structure of the Realizer associated to the current goal.Variants:
-
Program_all
Is equivalent to Repeat (Program Orelse Auto) (see section 7.14).
See also: chapter 18