Instantly share code, notes, and snippets.

View rotate.py
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]
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
View checking.py
#!/usr/bin/python
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
View join_quoted_strs.py
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
else:
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 = self.base.next() else { break }
self.skippedElements.append(element)
}
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)
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
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
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)