DreamLinuxer

⟪ ⇒ ∣
(uniti₊l ⊚ swap₊) ⊚
(id↔ ⊕ η) ⊚
(assocl₊ ⊚ (swap₊ ⊕ id↔) ⊚ assocr₊) ⊚ (id↔ ⊕ ε) ⊚ swap₊ ⊚ unite₊l
⟦ 𝔽 ⟧⟫
∷
⟪ ⇒ ∣
(id↔ ⊚ swap₊) ⊚
(id↔ ⊕ η) ⊚
(assocl₊ ⊚ (swap₊ ⊕ id↔) ⊚ assocr₊) ⊚ (id↔ ⊕ ε) ⊚ swap₊ ⊚ unite₊l

DreamLinuxer

⟪ ⇒ ∣
dist ⊚
(uniti₊l ⊚ swap₊) ⊚
(id↔ ⊕ η) ⊚
(assocr₊ ⊚ (id↔ ⊕ (assocl₊ ⊚ (swap₊ ⊕ id↔) ⊚ assocr₊)) ⊚ assocl₊) ⊚
((id↔ ⊕
  (id↔ ⊗
   ((id↔ ⊗ swap₊) ⊚
    (swap⋆ ⊚ dist ⊚ (swap⋆ ⊕ swap⋆)) ⊚
    ((swap₊ ⊗ id↔) ⊕ id↔) ⊚ (swap⋆ ⊕ swap⋆) ⊚ factor ⊚ swap⋆)))

DreamLinuxer

data Zero
data One = TT
data 𝔹 = 𝔽 | 𝕋 
data T = C1 | C2 (𝔹,𝔹)

f :: T <-> T
f C1         = C2 (𝔽,𝔽)
f (C2 (𝕋,x)) = C2 (x,𝕋)
f (C2 (𝔽,𝔽)) = C1
f (C2 (𝔽,𝕋)) = C2 (𝕋,𝔽)

DreamLinuxer

(require 'haskell-interactive-mode)
(require 'haskell-process)
(add-hook 'haskell-mode-hook 'turn-on-haskell-doc-mode)
(add-hook 'haskell-mode-hook '(lambda () (local-set-key (kbd "RET") 'newline-and-indent)))
(add-hook 'haskell-mode-hook 'interactive-haskell-mode)

(custom-set-variables
 '(haskell-process-auto-import-loaded-modules (quote t))
 '(haskell-process-log (quote t))
 '(haskell-process-suggest-remove-import-lines (quote t))

DreamLinuxer

pub trait Encoding {
    fn encode (b : bool) -> Self;
    fn decode (&self) -> bool;
}

pub trait Comp : Encoding {
    fn and(l:Self,r:Self) -> Self;
}

fn test<T : Comp> (l:T,r:T) -> T {

DreamLinuxer

#!/usr/bin/env python
import subprocess32 as subprocess
import sys
import os

test_inputs = [[4,1,1],[6,2,3],[8,4,4],[11,9,8],[15,7,2]]

def get_name(s):
    return s[0:s.index('_')]

DreamLinuxer

{-@ LIQUID "--higherorder"        @-}
{-@ LIQUID "--totality"           @-}
{-@ LIQUID "--exactdc"            @-}

module Data.VerifiedMonoid.Instances.Prod ({-vmonoidProd-}) where

--import Data.VerifiedMonoid
import Language.Haskell.Liquid.ProofCombinators

{-@ axiomatize identProd @-}

DreamLinuxer

module T where

Ḳ : {X Y : Set} → X → Y → X
Ḳ x y = x

Ṣ : {X Y Z : Set} → (X → Y → Z) → (X → Y) → X → Z
Ṣ f g x = f x (g x)

_∘_ : {X Y Z : Set} → (Y → Z) → (X → Y) → (X → Z)
g ∘ f = λ x → g (f x)

DreamLinuxer

set datafile separator ","
set terminal postscript eps enhanced color font 'Helvetica,20'
set output 'cold-hot.eps'
set xrange [1:18]
set yrange [2000:20000]
set xlabel 'Thread number'
set ylabel 'ops/ms'

plot '1448725779_G0.5-I0.25_pure.csv' using 1:2:3 title 'PureMap' with yerrorlines pointtype 4 pointsize 2, '1448725779_G0.5-I0.25_ctrie.csv' using 1:2:3 title 'Ctrie' with yerrorlines pointtype 7 pointsize 2, '1448725779_G0.5-I0.25_adaptive.csv' using 1:2:3 title 'AdaptiveMap' with yerrorlines pointtype 8 pointsize 2

DreamLinuxer

module nat where
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

indℕ : ∀ {ℓ} → (C : ℕ → Set ℓ) → C 0 → ((n : ℕ) → C n → C (suc n)) → (n : ℕ) → C n
indℕ C z f 0 = z
indℕ C z f (suc n) = f n (indℕ C z f n)

iter : ∀ {ℓ} (C : Set ℓ) → C → (C → C) → ℕ → C