Skip to content

Instantly share code, notes, and snippets.

Jaden Geller JadenGeller

Block or report user

Report or block JadenGeller

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
JadenGeller /
Last active Jun 14, 2018
Rotate in place
def transpose_matrix(size, matrix):
for y in range(size):
for x in range(y):
matrix[y][x], matrix[x][y] = matrix[x][y], matrix[y][x]
def flip_y_matrix(size, matrix):
for y in range(size // 2):
flip_y = size - y - 1
for x in range(size):
matrix[x][y], matrix[x][flip_y] = matrix[x][flip_y], matrix[x][y]
JadenGeller / Constructive.idr
Created Apr 27, 2018
Are constructive programs better?
View Constructive.idr
import Data.List
import Data.List.Views
import Data.Vect
import Data.Vect.Views
%default total
-- Constructive
rotate : Vect len elem -> Vect len elem
JadenGeller /
Created Apr 2, 2018
Dynamic Type Checking
import inspect
def typeAsserting(f):
signature = inspect.signature(f)
def wrapper(*args, **kwargs):
bound_args = signature.bind(*args, **kwargs)
for name, parameter_value in bound_args.arguments.items():
expected_type = signature.parameters[name].annotation
JadenGeller /
Created Jan 24, 2018
A gross simple state machine
def join_quoted_strs(s):
r = ''
within_quotes = False
is_escaped = False
for c in s:
if within_quotes:
if is_escaped:
r += c
is_escaped = False
View TypeDictionary.swift
private struct TypeDescriptor: Hashable, CustomStringConvertible {
private let type: Any.Type
internal init(_ type: Any.Type) {
self.type = type
public var hashValue: Int {
return String(describing: type).hashValue
public static func ==(lhs: TypeDescriptor, rhs: TypeDescriptor) -> Bool {
View Advent1.swift
public struct RotatingIterator<Base: IteratorProtocol>: Sequence, IteratorProtocol {
private var skippedElements: [Base.Element] = []
private var base: Base
internal init(_ base: Base, count: Int) {
self.base = base
for _ in 0..<count {
guard let element = else { break }
View Advent.idr
import SignedNat
import Data.Vect
step : (Fin n, Vect n SignedNat) -> (SignedNat, Vect n SignedNat)
step (i, xs) = let delta = index i xs in
let xs' = updateAt i succ xs in
let i' = (toSignedNatNat (finToNat i)) + delta in
(i', xs')
signedNatToFin : SignedNat -> (m : Nat) -> Maybe (Fin m)
JadenGeller / SignedNat.idr
Created Dec 17, 2017
Signed Natural Numbers
View SignedNat.idr
module SignedNat
import Control.Isomorphism
%access public export
%default total
||| Signed natural numbers: unbounded, signed integers which can be pattern
||| matched.
data SignedNat : Type where
JadenGeller / captcha.idr
Created Dec 12, 2017
Advent 2017 Day 1
View captcha.idr
import Data.Vect
import Data.Vect.Views
%default total
infixl 1 &
(&) : a -> (a -> b) -> b
x & f = f x
rotate : Vect len elem -> Vect len elem
JadenGeller / LEM.idr
Last active Mar 29, 2018
Derivation of Law of the Excluded Middle from call/cc
View LEM.idr
%default total
postulate callCC : ((a -> Void) -> a) -> a
peirce : ((a -> b) -> a) -> a
peirce f = callCC (f . (void .))
notExcludedMiddleImpliesExcludedMiddle : Not (Dec p) -> Dec p
notExcludedMiddleImpliesExcludedMiddle notExcludedMiddle = No (notExcludedMiddle . Yes)
You can’t perform that action at this time.