From f5ca4613d7a4a69b562ffdfeaf8765aa5b0f8535 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Mon, 17 Feb 2020 23:55:43 -0500 Subject: [PATCH] preparing Ltac lecture --- IntroToProofScripting.v | 19 +++++++++++++++++++ TransitionSystems.v | 2 +- 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/IntroToProofScripting.v b/IntroToProofScripting.v index 7717a4b..af0aa45 100644 --- a/IntroToProofScripting.v +++ b/IntroToProofScripting.v @@ -483,6 +483,25 @@ Goal False. length (1 :: 2 :: 3 :: nil) ltac:(fun n => pose n). 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: *) +Module Import WithPrintingFixedWithoutContinuations. + Ltac length ls := + let __ := match constr:(Set) with + | _ => (* put all your side effects here:*) + idtac ls; assert (ls = ls) by equality + end in + match ls with + | nil => constr:(O) + | _ :: ?ls' => let L := length ls' in constr:(S L) + end. +End WithPrintingFixedWithoutContinuations. + +Goal False. + let n := length (1 :: 2 :: 3 :: nil) in + pose n. +Abort. (** * Recursive Proof Search *) diff --git a/TransitionSystems.v b/TransitionSystems.v index 41aec5e..eb50cb6 100644 --- a/TransitionSystems.v +++ b/TransitionSystems.v @@ -29,7 +29,7 @@ Inductive fact_state := * throughout recursive invocations of a predicate (though this definition does * not use recursion). After the colon, we give a type that expresses which * additional arguments exist, followed by [Prop] for "proposition." - * Putting this inductive definition in [Prop] is what marks at as a predicate. + * Putting this inductive definition in [Prop] is what marks it as a predicate. * Our prior definitions have implicitly been in [Set], the normal universe * of mathematical objects. *) Inductive fact_init (original_input : nat) : fact_state -> Prop :=