dagit

-- http://www.cs.swan.ac.uk/~csetzer/articlesFromOthers/chiMing/chiMingChuangExtractionOfProgramsForExactRealNumberComputation.pdf
module Real where

open import Data.Product renaming (_×_ to _∧_)

infixl 9 ─ recip
infixl 4 _*_
infixl 3 _+_ _#_
infixl 2 ∣_∣
infix  0 _==_ _≤_ _<_

dagit

-- http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms-extended.pdf
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE ScopedTypeVariables   #-}

module ZipWith (zipWith) where

dagit

/*===-- llvm-c/Core.h - Core Library C Interface ------------------*- C -*-===*\
|*                                                                            *|
|*                     The LLVM Compiler Infrastructure                       *|
|*                                                                            *|
|* This file is distributed under the University of Illinois Open Source      *|
|* License. See LICENSE.TXT for details.                                      *|
|*                                                                            *|
|*===----------------------------------------------------------------------===*|
|*                                                                            *|
|* This header declares the C interface to libLLVMCore.a, which implements    *|

dagit

module FilterExamples where
  data Bool : Set where
    true false : Bool -- two constructors, true and false

  data List (A : Set) : Set where
    []  : List A
    _∷_ : A → List A → List A

  [_] : {A : Set} → A → List A
  [ a ] = a ∷ []

dagit

$ ghci -fno-ghci-sandbox -package GLFW-b -v
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Glasgow Haskell Compiler, Version 7.6.3, stage 2 booted by GHC version 7.4.2
Using binary package database: /Users/dagit/local-install/lib/ghc-7.6.3/package.conf.d/package.cache
Using binary package database: /Users/dagit/.ghc/x86_64-darwin-7.6.3/package.conf.d/package.cache
wired-in package ghc-prim mapped to ghc-prim-0.3.0.0-d5221a8c8a269b66ab9a07bdc23317dd
wired-in package integer-gmp mapped to integer-gmp-0.5.0.0-2f15426f5b53fe4c6490832f9b20d8d7
wired-in package base mapped to base-4.6.0.1-6c351d70a24d3e96f315cba68f3acf57
wired-in package rts mapped to builtin_rts
wired-in package template-haskell mapped to template-haskell-2.8.0.0-c2c1b21dbbb37ace4b7dc26c966ec664

dagit

$ ghci -fno-ghci-sandbox -package GLFW-b -v
GHCi, version 7.6.3: http://www.haskell.org/ghc/  :? for help
Glasgow Haskell Compiler, Version 7.6.3, stage 2 booted by GHC version 7.4.2
Using binary package database: /Users/dagit/local-install/lib/ghc-7.6.3/package.conf.d/package.cache
Using binary package database: /Users/dagit/.ghc/x86_64-darwin-7.6.3/package.conf.d/package.cache
wired-in package ghc-prim mapped to ghc-prim-0.3.0.0-d5221a8c8a269b66ab9a07bdc23317dd
wired-in package integer-gmp mapped to integer-gmp-0.5.0.0-2f15426f5b53fe4c6490832f9b20d8d7
wired-in package base mapped to base-4.6.0.1-6c351d70a24d3e96f315cba68f3acf57
wired-in package rts mapped to builtin_rts
wired-in package template-haskell mapped to template-haskell-2.8.0.0-c2c1b21dbbb37ace4b7dc26c966ec664

dagit

/*
From Section 11.2: http://www.jn.inf.ethz.ch/education/script/P3_C11.pdf

a, b, and c, are meant to be square matrices of booleans. We couldn't use bool from stdbool.h because
haskell doesn't have a CBool type

*/
void mult(char * a, char * b, char * c, int sz) {
  int i,j,k,ij,ik,kj;
  for(i = 0; i < sz; i++){

dagit

module HList where

open import Level
open import Data.Bool
open import Data.Nat hiding (_⊔_)
open import Data.Vec
open import Data.List

data HList {a} : List (Set a) → Set (Level.suc a) where
  []  : HList []

dagit

module Bug where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

cong : ∀ {A : Set} {B : Set}

dagit

# 
METHOD: TABLE
ENCODE: Unicode
PROMPT: TeX 1.2
VERSION: 1.2
DELIMITER: ,
MAXCODE: 6
VALIDINPUTKEY: ^,.?!:;"'/\()[]{}<>$%&@*01234567890123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz
TERMINPUTKEY: 
BEGINCHARACTER