trillioneyes

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)

trillioneyes

-- λΠ> 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

module TuringMachine

trillioneyes

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

;; 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)

trillioneyes

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."