bond15

module TM where
open import Data.Integer

data V : Set where
    One Zero Empty : V

data HeadDir : Set where
    L R : HeadDir
 
-- An encoding of Polynomial Functors

rxwei

See the official Differentiable Programming Manifesto instead.

robey

;
; the "monitor ROM" of an apple 1 fit in one page (256 bytes).
;
; this is my attempt to take the disassembled code, give names to the
; variables and routines, and try to document how it worked.
;
;
; an apple 1 had 8KB of RAM (more, if you hacked on the motherboard), and a
; peripheral chip that drove the keyboard and video. the video was run by a
; side processor that could treat the display as an append-only terminal that

ddevault

WAYLAND_PROTOCOLS=/usr/share/wayland-protocols

# wayland-scanner is a tool which generates C headers and rigging for Wayland
# protocols, which are specified in XML. wlroots requires you to rig these up
# to your build system yourself and provide them in the include path.
xdg-shell-protocol.h:
	wayland-scanner server-header \
		$(WAYLAND_PROTOCOLS)/stable/xdg-shell/xdg-shell.xml $@

xdg-shell-protocol.c: xdg-shell-protocol.h

jmoy

section ‹A Simple Graph Problem›

text ‹
We shall prove the following: "In a finite group of people, some of whom are friends with some
of the others there must be at least two people who have the same number of friends."
›

theory Friends
  imports   Main 
            Finite_Set 

aparrish

mrkgnao

{-# LANGUAGE Arrows                 #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE InstanceSigs           #-}
{-# LANGUAGE LambdaCase             #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE ScopedTypeVariables    #-}

mrkgnao

module Main

import Data.Vect

-- %hide transpose

dot : Num a => Vect n a -> Vect n a -> a
dot va vb = foldr (+) 0 $ zipWith (*) va vb

Matrix : (rows : Nat) -> (cols : Nat) -> Type -> Type

thomasstoeckert

RacerX
10/26/2016

Thomas Stoeckert
11/30/2016

Thomas Stoeckert
1/26/2018

WSL pebble building

jtobin

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}

import Control.Comonad
import Control.Comonad.Cofree
import Control.Monad
import Control.Monad.ST