Skip to content

Instantly share code, notes, and snippets.

MaiaVictor

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

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

package.json

{
    "fileType": "SpriteStackModelProject",
    "title": "Whatever"
}
@takanuva
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) ->
N
@cheery
cheery / interaction_combinators.py
Created Mar 28, 2019
Interaction combinators
View interaction_combinators.py
# -*- 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
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
variable
m n :
b : Bool
Γ Δ Ξ T I O : Vec Bool n
@AndrasKovacs
AndrasKovacs / AB.agda
Last active Sep 11, 2018
Solution to SO question
View AB.agda
-- https://stackoverflow.com/questions/52244800/how-to-normalize-rewrite-rules-that-always-decrease-the-inputs-size/52246261#52246261
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
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:
https://hub.darcs.net/dolio/agda-share/browse/ParamInduction.agda.
*)
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
onlurking / infinite.py
Last active Mar 6, 2018
generate all possible strings under 20 lines of Python
View infinite.py
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
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
codedot / Makefile
Last active May 21, 2018
Bitcoin proof of work in pure lambda calculus
View Makefile
all:
node work2mlc.js getwork.json 381353fa >test.mlc
lambda -pem lib.mlc -f test.mlc
clean:
You can’t perform that action at this time.