Skip to content

Instantly share code, notes, and snippets.

Miles Rout milesrout

Block or report user

Report or block milesrout

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
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.