kencoba

(comment
 this code uses http://clojars.org/clj-time.)

(ns palindrome-date-time.core
  (:require [clj-time.core :as t])
  (:require [clj-time.format :as f]))

(def custom-formatter (f/formatter "yyyyMMdd"))

(defn date-seq [d]

kencoba

(ns logic
  (:use [clojure.test]))

(defmacro implies [p q] `(or (not ~p) ~q))

(deftest test-implies
  (are [e p q] (= e (implies p q)) 
       true true true
       false true false
       true false true

kencoba

Inductive day : Type :=
  | monday : day
  | tuesday : day
  | wednesday : day
  | thursday : day
  | friday : day
  | saturday : day
  | sunday : day.

Definition next_weekday (d:day) : day :=

kencoba

Require Export Basics.

Module NatList.

Inductive natprod : Type :=
  pair : nat -> nat -> natprod.

Definition fst (p:natprod):nat :=
  match p with
    | pair x y => x

kencoba

Require Export ConCaT.CATEGORY_THEORY.CATEGORY.Category.

Set Implicit Arguments.
Unset Strict Implicit.

Inductive Two_ob : Type :=
  | obone : Two_ob
  | obtwo : Two_ob.

Inductive Two_mor : Two_ob -> Two_ob -> Type :=

kencoba

theory ToyList
imports Datatype
begin

datatype 'a list = Nil ("[]")
| Cons 'a "'a list"    (infixr "#" 65)

(* This is append function: *)
primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
where

kencoba

(defn- charlist-to-digits [lst]
  (map #(Integer/parseInt %)
    (map #(str (first %))
      (partition 1 2 lst))))

(defn- odd-digits [card-num]
  (charlist-to-digits (reverse card-num)))

(defn- even-digits [card-num]
  (charlist-to-digits (rest (reverse card-num))))

kencoba

Section NaturalDeduction_p18.
  Variable D : Set.
  Variable P : D -> D -> Prop.
  Hypothesis Pxy : forall x, exists y, P x y.
  Hypothesis PxyPyx : forall x y,(P x y) -> (P y x).

  Lemma p18 : forall x, exists y, (P x y) /\ (P y x).
  Proof.
    intros x.
    elim (Pxy x).

kencoba

open util/relation

sig P {
	f : one X,
	f_bar : one E
}
sig E {
	e : one X
}
sig X {}

kencoba

(ns casl-assembler
  (:use [clojure.test :only (deftest is run-tests)]
        [clojure.contrib.str-utils :only (re-split)]))

(def prog0
     [
      "PROG1 START GO"
      "DATA1 DC    1"
      "DATA2 DC    2"
      "ANS   DS    1"