Skip to content

Instantly share code, notes, and snippets.

Miles Rout milesrout

View GitHub Profile
View actuallygood.agda
data _⊔_is_ : ℕ → ℕ → ℕ → Set where
m≥⊔nism : {m n : ℕ}
n ≤ m
---------
m ⊔ n is m
m≤⊔nisn : {m n : ℕ}
m ≤ n
---------
m ⊔ n is n
View meme.agda
data ℕ : Set where
zero :
suc :
{-# BUILTIN NATURAL ℕ #-}
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ}
-------
zero ≤ n
View input.b
DEBUG = True
macro ASSERT(e):
return \(if DEBUG:
if not $e:
raise AssertionError($(stringify(e))))
def assert_equal(x, z):
# x and z are compared so they must have the same type
View gist:b1f72726dc48c5201901aba3de40ff5e
# normal macro
# \ is ` and $ is ,
macro assert(e):
\(if DEBUG:
if not $e:
raise AssertionError($(stringify(e)))
# control structure macro
View gist:f14eaf7ffeb37a70fca9ffc9cd233382
# normal macro
# \ is ` and $ is ,
macro assert(e):
\(if DEBUG:
if not $e:
raise AssertionError($(stringify(e)))
# control structure macro
View gist:625de4852f7756e9e6443a88f637fc08
data X = X { _y :: Y }
data Y = Y1 { _y1 :: Int }
| Y2 { _y2 :: String }
x1 = X (Y1 0)
x2 = X (Y2 "Hello")
i1 = x1^.y.y1 -- error ??
i2 = x2^.y.y1 -- error ??
s1 = x1^.y.y2
@milesrout
milesrout / tclass.py
Created Oct 9, 2018 — forked from louisswarren/tclass.py
Extension of inheriting from namedtuple
View tclass.py
def tclass(*argnames, then_do=None):
if len(argnames) == 1 and isinstance(argnames[0], dict):
argnames = argnames[0]
def decorator(cls):
def inner_init(self, *args, **kwargs):
for argname, arg in zip(argnames, args):
self.__setattr__(argname, arg)
for argname in list(argnames)[len(args):]:
self.__setattr__(argname, argnames[argname])
@milesrout
milesrout / DCPU-16N.txt
Created Aug 25, 2018 — forked from Meisaka/DCPU-16N.txt
DCPU redesigns
View DCPU-16N.txt
DCPU-16N Specification
Copyrights 1985 Mojang, Meisaka Yukara
Version 0.14 influenced by DCPU-16 (1.7)
=================================== SUMMARY ====================================
* 16 bit CISC CPU design
* DCPU-16 compatibility functions
* 8/16 bit switchable memory word size (1 octet per address or 2 octets per address)
View test_scanner.py
import collections
import difflib
import pathlib
import dill as pickle
import scanner
import sys
import utils
Token = collections.namedtuple('Token', 'line col type string virtual')
View gist:ce51566cc62c34d2863dd553527b64cf
Akaroa
Amuri
Ashburton
Bay of Islands
Bruce
Buller
Chatham Islands
Cheviot
Clifton
Clutha
You can’t perform that action at this time.