Commits

Paweł Wieczorek committed 176a78f

* Usunięcie niepotrzebnych plików

Comments (0)

Files changed (4)

 # $Id$
-COQ_MAKEFILE= coq_makefile -I .
+COQ_MAKEFILE= coq_makefile -R metalogic metalogic
 GEN_MAKEFILE= Makefile.Coq
 SOURCES= `find . -name \*.v`
 WRAPED_MAKE= ${MAKE} -f ${GEN_MAKEFILE}

metalogic/Pc/Proof_facts.v

  assumption.
 Qed. 
 
-
+(*
 Theorem PcDeduction: forall T p q,
   (T |- p --> q)   <->  (T, p |- q).
 Proof.
 destruct PrfT.
 
 intros. 
-Qed.
+Qed.
+
+*)

metalogic/Util/Ensemble_facts.v

-Require Import Sets.Ensembles.
-
-
-(*
- * (A + B) + C = 
- *)
-Theorem U {T:Type}: forall T A B C: 

metalogic/Util/Seq.v

-
-Section Seq.
-
-Inductive ProofSeq : Type :=
-| Seq_intro: nat -> (nat -> pcProp) -> ProofSeq
-.
-
-(*
-Definition nth n (xs:Seq default) :=
-match xs with Seq_intro N f =>
-match (N-n) with
-| 0 => default
-| _ => f n
-end end.
-
-Definition append (xs:Seq default) (ys:Seq default) := 
-match (xs,ys) with
- (Seq_intro xN xF, Seq_intro yN yF) =>
-  let f n := match (xN - n)  with
-      | 0 => yF (n - xN)
-      | _ => xF n
-      end in Seq_intro default (xN + yN) f
-end.
-
-Definition last (xs:Seq default) :=
-match xs with
- (Seq_intro N F) => F (N-1)
-end.
-
-Definition head (xs:Seq default) :=
-match xs with
- (Seq_intro N F) => F 0
-end.
-
-Definition tail (xs:Seq default) :=
-match xs with
- (Seq_intro N F) => Seq_intro default (N-1) (fun n => F (n+1))
-end.
-*)
-
-End Seq.
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.