pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for Wednesday's lecture

Browse source
This commit is contained in:
Adam Chlipala 2022-02-13 14:34:23 -05:00
parent 0cba7c9f61
commit 23a0972d11
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
IntroToProofScripting.v
View file

@ -12,7 +12,7 @@ Set Implicit Arguments.
(** * Ltac Programming Basics *)
(* We have already seen a few examples of Ltac programs, without much explanation.
* Ltac is the proof scripting language built into Coq. Actually, every
* Ltac is the proof-scripting language built into Coq. Actually, every
* primitive step in our proofs has been a (degenerate, small) Ltac program.
* Let's take a bottom-up look at more Ltac features.
*
@ -245,7 +245,7 @@ Qed.
(* In class, we develop our own implementation of [propositional] one feature
* at a time, but here's just the final product. To understand it, we print
* the definitions of the logical connectives. Interestingly enough, they are
* special cases of the machinery we met last time for inductive relations! *)
* special cases of the machinery we met previously for inductive relations! *)
Print True.
Print False.
@ -485,7 +485,7 @@ Abort.
(* However, it's not always convenient to use continuation-passing style
* everywhere, so cool kids use the following hack to sneak side effects
* into otherwise functional Ltac code. *)
* into otherwise-functional Ltac code. *)
Module Import WithPrintingFixedWithoutContinuations.
Ltac length ls :=
let __ := match constr:(Set) with
@ -503,6 +503,7 @@ Goal False.
pose n.
Abort.
(** * Recursive Proof Search *)
(* Let's work on a tactic to try all possible instantiations of quantified