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))