Skip to content

Instantly share code, notes, and snippets.


Block or report user

Report or block MaiaVictor

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
rezoner /
Last active Jan 8, 2020
SpriteStack format specs draft

A spritestack model is a ZIP file with two obligatory entries:


    "fileType": "SpriteStackModelProject",
    "title": "Whatever"
takanuva / Church
Last active Mar 11, 2020
Conversion between Scott encoding and Church endocing for naturals in CoC
View Church
\/(N: *) ->
\/(z: N) ->
\/(s: N -> N) ->
cheery /
Created Mar 28, 2019
Interaction combinators
# -*- encoding: utf-8 -*-
# Implements symmetric interaction combinators
# I took some ideas from Victor Maia's projects.
# Bunch of cells form an interaction net.
# It's a half-edge graph.
class Cell:
def __init__(self, kind):
self.ports = (Port(self), Port(self), Port(self))
self.kind = kind # 'era', 'con', 'fan'
gallais / linear.agda
Last active Mar 26, 2019
Raw linear terms
View linear.agda
open import Data.Nat.Base
open import Data.Vec
open import Data.Bool.Base using (Bool; false; true)
open import Data.Product
m n :
b : Bool
Γ Δ Ξ T I O : Vec Bool n
AndrasKovacs / AB.agda
Last active Sep 11, 2018
Solution to SO question
View AB.agda
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Relation.Nullary
open import Data.Empty
open import Data.Star
data AB : Set where
A : AB -> AB
takanuva / proj.v
Created Aug 1, 2018
Admissibility of strong projections
View proj.v
Prove that, due to the free theorem for impredicative sigma types, strong
projection is a valid extension. Based on Dan Doel's Agda version:
Definition Rel (A: Prop) (B: Prop) :=
A -> B -> Prop.
Definition Sigma (T: Prop) (U: T -> Prop): Prop :=
View all_strings.cpp
// generator.cpp : Defines the entry point for the console application.
#include "stdafx.h"
#include <experimental\generator>
#include <string>
#include <numeric>
#include <vector>
#include <cstdint>
#include <sstream>
onlurking /
Last active Mar 6, 2018
generate all possible strings under 20 lines of Python
from itertools import count, product
from string import digits, ascii_lowercase, ascii_uppercase
from sys import stdout
import argparse
combinations = ascii_lowercase
parser = argparse.ArgumentParser()
parser.add_argument("--digits", "-d", help="include numbers", action="store_true")
parser.add_argument("--upper", "-u", help="include uppercase letters", action="store_true")
args = parser.parse_args()
nkaretnikov / .emacs
Last active Mar 16, 2018
Agda .emacs
View .emacs
(add-to-list 'load-path "~/.emacs.d/evil")
(require 'evil)
(evil-mode 1)
;; Highlight matching parens.
(show-paren-mode 1)
;;; No tabs.
(setq-default ident-tabs-mode nil)
(setq-default tab-width 4)
codedot / Makefile
Last active May 21, 2018
Bitcoin proof of work in pure lambda calculus
View Makefile
node work2mlc.js getwork.json 381353fa >test.mlc
lambda -pem lib.mlc -f test.mlc
You can’t perform that action at this time.