mirror of
https://github.com/achlipala/frap.git
synced 2024-11-10 00:07:51 +00:00
Merge branch 'master' of github.com:achlipala/frap
This commit is contained in:
commit
c2f56e1b5f
3 changed files with 21 additions and 2 deletions
|
@ -483,6 +483,25 @@ Goal False.
|
||||||
length (1 :: 2 :: 3 :: nil) ltac:(fun n => pose n).
|
length (1 :: 2 :: 3 :: nil) ltac:(fun n => pose n).
|
||||||
Abort.
|
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 *)
|
(** * Recursive Proof Search *)
|
||||||
|
|
||||||
|
|
|
@ -182,7 +182,7 @@ Section propositional.
|
||||||
Admitted.
|
Admitted.
|
||||||
End propositional.
|
End propositional.
|
||||||
|
|
||||||
(* Backrtracking example #1 *)
|
(* Backtracking example #1 *)
|
||||||
|
|
||||||
Theorem m1 : True.
|
Theorem m1 : True.
|
||||||
Proof.
|
Proof.
|
||||||
|
|
|
@ -29,7 +29,7 @@ Inductive fact_state :=
|
||||||
* throughout recursive invocations of a predicate (though this definition does
|
* throughout recursive invocations of a predicate (though this definition does
|
||||||
* not use recursion). After the colon, we give a type that expresses which
|
* not use recursion). After the colon, we give a type that expresses which
|
||||||
* additional arguments exist, followed by [Prop] for "proposition."
|
* 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
|
* Our prior definitions have implicitly been in [Set], the normal universe
|
||||||
* of mathematical objects. *)
|
* of mathematical objects. *)
|
||||||
Inductive fact_init (original_input : nat) : fact_state -> Prop :=
|
Inductive fact_init (original_input : nat) : fact_state -> Prop :=
|
||||||
|
|
Loading…
Reference in a new issue