Skip to content

Instantly share code, notes, and snippets.

module NonBlocking
-- this is what I'd ideally like to do, and it seems like it should
-- work -- but it doesn't
requestAnimationFrame : (Float -> JS_IO ()) -> JS_IO ()
requestAnimationFrame act = foreign FFI_JS
"requestAnimationFrame(%0)"
(JsFn (Float -> JS_IO ()) -> JS_IO ())
(MkJsFn act)
-- λΠ> run $ the (SideEffect FFI_JS ()) (run yieldDemo)
io_bind (io_bind (MkIO (\w =>
mkForeignPrim (JS_Str, "red") w "setColor(%0)" JS_Unit))
(\ {bindx9} =>
MkIO (\w =>
mkForeignPrim (JS_IntT JS_IntNative, 50)
(JS_IntT JS_IntNative, 50)
(JS_IntT JS_IntNative, 0)
(JS_IntT JS_IntNative, 0)
w
@trillioneyes
trillioneyes / TuringMachine.idr
Created October 30, 2014 14:42
Turing machines in Idris
module TuringMachine
@trillioneyes
trillioneyes / Sublist.idr
Last active August 29, 2015 14:08
Preorder Reasoning Examples
module Sublist
import Syntax.PreorderReasoning
%default total
data Sublist : List a -> List a -> Type where
Keep : Sublist xs ys -> Sublist (x::xs) (x::ys)
Drop : Sublist xs ys -> Sublist xs (y::ys)
Vacuous : Sublist [] ys
@trillioneyes
trillioneyes / multinarrow.lisp
Created September 11, 2014 17:48
Define advice for `narrow-to-region` so that it will automatically create an indirect buffer
;; Make narrowing nicer
; this makes sure we have a way to get the name of the current function
(which-function-mode)
(defadvice narrow-to-defun (before narrow-in-new-buffer activate)
"When using `narrow-to-defun', narrow in an indirect buffer whose
name is the original buffer's name augmented by the function
being focused."
(let ((parent-name (buffer-name))
(name (concatenate 'string
(buffer-name)
import XMonad.ManageHook ((-->))
hands :: Int
hands = 5 + undefined
complaint :: Int -> String
complaint _ = "Lots of things are red now for no reason. Also, strings aren't highlighted right."