Mercurial > cpdt > repo
comparison src/LogicProg.v @ 534:ed829eaa91b2
Builds with Coq 8.5beta2
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 05 Aug 2015 14:46:55 -0400 |
parents | 05c0f872a129 |
children | 8dddcaaeb67a |
comparison
equal
deleted
inserted
replaced
533:8921cfa2f503 | 534:ed829eaa91b2 |
---|---|
1 (* Copyright (c) 2011-2012, Adam Chlipala | 1 (* Copyright (c) 2011-2012, 2015, Adam Chlipala |
2 * | 2 * |
3 * This work is licensed under a | 3 * This work is licensed under a |
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
5 * Unported License. | 5 * Unported License. |
6 * The license text is available at: | 6 * The license text is available at: |
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ | 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ |
8 *) | 8 *) |
9 | 9 |
10 (* begin hide *) | 10 (* begin hide *) |
11 | 11 |
12 Require Import List. | 12 Require Import List Omega. |
13 | 13 |
14 Require Import CpdtTactics. | 14 Require Import Cpdt.CpdtTactics. |
15 | 15 |
16 Set Implicit Arguments. | 16 Set Implicit Arguments. |
17 | 17 Set Asymmetric Patterns. |
18 (* end hide *) | 18 (* end hide *) |
19 | 19 |
20 (** %\part{Proof Engineering} | 20 (** %\part{Proof Engineering} |
21 | 21 |
22 \chapter{Proof Search by Logic Programming}% *) | 22 \chapter{Proof Search by Logic Programming}% *) |
683 (* begin thide *) | 683 (* begin thide *) |
684 eauto. | 684 eauto. |
685 Qed. | 685 Qed. |
686 (* end thide *) | 686 (* end thide *) |
687 | 687 |
688 (* begin hide *) | |
689 (* begin thide *) | |
690 Definition e1s := eval1'_subproof. | |
691 (* end thide *) | |
692 (* end hide *) | |
693 | |
694 Print eval1'. | 688 Print eval1'. |
695 (** %\vspace{-.15in}%[[ | 689 (** %\vspace{-.15in}%[[ |
696 eval1' = | 690 eval1' = |
697 fun var : nat => | 691 fun var : nat => |
698 EvalPlus' (EvalVar var) (EvalPlus (EvalConst var 8) (EvalVar var)) | 692 EvalPlus' (EvalVar var) (EvalPlus (EvalConst var 8) (EvalVar var)) |