konn

header{*The Rational Numbers as Equivalence Classes Over Pairs of Integers*}
theory Rat_ZF
imports "~~/src/ZF/Main_ZFC" "~~/src/ZF/Int_ZF" begin
definition
  ratrel :: i where
    "ratrel \<equiv> { < <x1, x2>, <y1, y2> > \<in> (int*int)*(int*int) .
                x1 $* y2 = x2 $* y1 }"
definition
  rat :: i where
    "rat \<equiv> (int*int)//ratrel - {<z, $#0> . z \<in> int}"

konn

module Main where
               (<))
import Prelude (Num(..),

konn

   Glob-0.7.3
   ListLike-3.1.7.1
   MonadCatchIO-transformers-0.3.1.0
   MonadRandom-0.1.12
   abstract-deque-0.2.2
   abstract-par-0.3.3
   adjunctions-3.2.1.1
   aeson-0.7.0.0
   algebra-3.1
   ansi-terminal-0.6.1

konn

russel : (P : a -> a -> Type) -> Exists _ (\y => (x : a) -> (P x y -> (P x x -> _|_), (P x x -> _|_) -> P x y)) -> _|_
russel P (x ** f) with (f x)
  russel P (x ** f) | (a, b) = let a' = \x => a x x in a' (b a')

konn

angular.module('compile', [], function($compileProvider) {
     $compileProvider.directive('compile', function($compile) {
       return function(scope, element, attrs) {
         scope.$watch(
           function(scope) {
             return scope.$eval(attrs.compile);
           },
           function(value) {
	       var re = /\[\s*(\d+)\s*\]/g;
	       var numArr;

konn

module anonsum
import Syntax.PreorderReasoning
import Data.HVect

%default total

data Sum : Vect n Type -> Type where
  Inj : (k : Fin n) -> index k ts -> Sum ts

cons : a -> List a -> List a

konn

module FOL
import Syntax.PreorderReasoning

succAndOne : (n : Nat) -> plus n 1 = S n
succAndOne n = ?succAndOne_rhs

record Language : Type where
  LanguageDef : (funSym : Type)-> (predSym : Type) ->
                (funArity : funSym -> Nat) -> (predArity : predSym -> Nat) -> Language

konn

import Syntax.PreorderReasoning
G : Type
m : G -> G -> G
n : G -> G -> G
u_m : G
u_n : G
postulate m_unit_l : (x : G) -> (m u_m x = x)
postulate m_unit_r : (x : G) -> (m x u_m = x)
postulate n_unit_l : (x : G) -> (n u_n x = x)
postulate n_unit_r : (x : G) -> (n x u_n = x)

konn

#!/usr/bin/env perl
$latex            = 'uplatex -synctex=1';
$latex_silent     = 'uplatex -synctex=1';
$bibtex           = 'pbibtex';
$biber            = 'biber --bblencoding=utf8 -u -U --output_safechars';
$dvipdf           = 'dvipdfmx %O -o %D %S';
$makeindex        = 'mendex %O -o %D %S';
$max_repeat       = 5;
$pdf_mode	  = 3; # generates pdf via dvipdfmx

konn

module ZFC

class Set univ where
  member   : univ -> univ -> Type

data ExistsUnique : (a : Type) -> (P : a -> Type) -> Type where
  ExUniq_intro : {P : a -> Type} -> (x : a) -> P x -> ((y : a) -> P y -> x = y) -> ExistsUnique a P

getUniqWitness : {P : a -> Type} -> ExistsUnique a P -> a
getUniqWitness (ExUniq_intro a _ _) = a