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

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

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

   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

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

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

This is XeTeX, Version 3.1415926-2.5-0.9999.3 (TeX Live 2013)
 \write18 enabled.
entering extended mode
(./03-forcing-introduction.tex
LaTeX2e <2011/06/27>
Babel <3.9h> and hyphenation patterns for 78 languages loaded.
(/usr/local/texlive/2013/texmf-dist/tex/latex/bxjscls/bxjsarticle.cls
Document Class: bxjsarticle 2013/10/03 v0.9pre BXJS document classes
(/usr/local/texlive/2013/texmf-dist/tex/latex/tools/calc.sty)
(/usr/local/texlive/2013/texmf-dist/tex/latex/graphics/keyval.sty)

konn

PREDEF:
  - preface.re

CHAPS:
  - part1.re:
      - ch01.re
  - part2.re:
      - ch02.re

# POSTDEF:

konn

{-# LANGUAGE BangPatterns, OverloadedStrings #-}
module Main where
import           Data.ByteString       (breakSubstring)
import           Data.ByteString.Char8 (ByteString, inits, tails)
import qualified Data.ByteString.Char8 as BS
import           Data.List             (nub, sortBy)
import           Data.Monoid           ((<>))
import           Data.Ord              (comparing)

isPalindrome :: ByteString -> Bool

konn

module Moon where

data Monkey = WooKie

foo :: Bool -> String
foo True = show WooKie