7.12 Developing certified programs

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 17 and references [80, 81] 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 17. 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 17, section 19.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:
  1. Program_all
    Is equivalent to Repeat (Program Orelse Auto with *) (see section 7.14).

See also: chapter 17