{{ message }}

Instantly share code, notes, and snippets.

# Ting-gan LUA banacorn

Created Nov 4, 2020
View first.ml
 let first p xs = let length = Array.length xs in (* mutable aray index *) let i = ref 0 in (* there are no loop breaks in OCaml anyway *) let break = ref false in while not (!break) && !i < length do if p (xs.(!i)) then break := true else i := (!i) + 1 done; !i
Last active Aug 25, 2020
View Chapter-1-6.hs
 -- This exercise covers the first 6 chapters of "Learn You a Haskell for Great Good!" -- Chapter 1 - http://learnyouahaskell.com/introduction -- Chapter 2 - http://learnyouahaskell.com/starting-out -- Chapter 3 - http://learnyouahaskell.com/types-and-typeclasses -- Chapter 4 - http://learnyouahaskell.com/syntax-in-functions -- Chapter 5 - http://learnyouahaskell.com/recursion -- Chapter 6 - http://learnyouahaskell.com/higher-order-functions -- Download this file and then type ":l Chapter-1-6.hs" in GHCi to load this exercise
Last active Aug 19, 2020
View FLOLAC-STLC2.agda
 Intrinsically-typed de Bruijn representation of simply typed lambda calculus ============================================================================ \begin{code} open import Data.Nat open import Data.Empty hiding (⊥-elim) open import Relation.Nullary open import Relation.Binary.PropositionalEquality
Last active Jun 8, 2020
BuckleScript bindings for EventEmitter3 https://github.com/primus/eventemitter3
View EventEmitter3.re
 // // Types // type t; type eventName = string; type listener('a) = 'a => unit; type listener2('a, 'b) = ('a, 'b) => unit; type listener3('a, 'b, 'c) = ('a, 'b, 'c) => unit;
Last active Aug 8, 2019
View WAT.agda
 {-# OPTIONS --without-K #-} module A where infixl 4 _≡_ data _≡_ {A : Set} (x : A) : A → Set where refl : x ≡ x J : (A : Set) (C : (x y : A) → x ≡ y → Set) → ((x : A) → C x x refl)
Last active Aug 1, 2019
Reducing expressions in CP
View cp-reduction.md

# Reducing expressions in CP

## Background

CP is a process calculus presented by Philip Wadler in his paper "Propositions as sessions" (https://dl.acm.org/citation.cfm?id=2364568), as an attempt to bridge π-calculus with Linear logic.

Process calculus (like CP) provides a mean of modelling and describing the interactions and communications between a bunch of independent processes. The interaction between these processes are often described with some reduction rules.

Last active Oct 30, 2018
HC to TSP
View TSP.md

### Goal: show that TSP is NP-complete

• TSP is NP
• TSP is NP-Hard

### TSP is NP

• Algorithm: given a tour, sum the weights, and see if it exceeds the bound
• The verifier runs in polynomial time
Created Oct 1, 2018
node-gyp is problematic
View gist:0b10f5a029ae10d7cf9e81d5baed90f7
 \$ apm rebuild Rebuilding modules ✗ gyp info it worked if it ends with ok gyp verb cli [ '/Applications/Atom.app/Contents/Resources/app/apm/bin/node', gyp verb cli '/Applications/Atom.app/Contents/Resources/app/apm/node_modules/.bin/node-gyp', gyp verb cli 'rebuild' ] gyp info using node-gyp@3.4.0 gyp info using node@8.9.3 | darwin | x64 gyp verb command rebuild [] gyp verb command clean []
Created Aug 2, 2018
Developing Agda with Stack
View agda-stack.md

# Build

stack build --stack-yaml stack-8.4.3.yaml

# REPL

You may need to edit .ghci first:

Last active Jun 26, 2018
draft
record IsApplicative {ℓ} (F : Set ℓ → Set ℓ)
: Set (suc ℓ) where