Skip to content

Instantly share code, notes, and snippets.

View phantamanta44's full-sized avatar

phantamanta44

View GitHub Profile
@phantamanta44
phantamanta44 / fancy-vending.maude
Created January 26, 2023 04:22
mod FANCY-VENDING is
--- a single sort Q of states
sort Q .
--- a state may have no tokens...
op ø : -> Q [ctor] .
--- ...or it may have one token of some kind...
ops $ $c q qc m&m orr cok : -> Q [ctor] .
--- ...or it may be the union of two such states
op _ _ : Q Q -> Q [ctor assoc comm id: ø] .
@phantamanta44
phantamanta44 / hott_skribbl.csv
Created August 5, 2022 16:30
absurd adjunction affine connection Agda axiom axiom of choice baba blahaj category cobordism cofinality coherence composition contractible coproduct cosheaf directed graph emacs embedding equivalence extensionality fibration functorial groupoid hcomp holonomy homothety homotopy Hopf fibration identity induction infinity groupoid interval loop space monadicity monodromy parallel transport path induction path over path proof proof assistant proof tree proposition pullback pushout quotient recursion reflexivity simplex smugcube substitution suspension torus total space transport truncation type type theory ultracategory univalence universe variable whiskering yoneda lemma
@phantamanta44
phantamanta44 / Cat.agda
Created February 27, 2022 02:00
module Lib.Cat where
open import Agda.Primitive using (Level; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality public
open import Lib.Eq using (subst-dep₂)
private
variable
ℓ ℓʹ : Level
@phantamanta44
phantamanta44 / gen_ll1.py
Created January 31, 2022 01:24
wynnatlas expression parser generator
#!/usr/bin/env python3
from abc import ABC
from collections import defaultdict
import itertools
import sys
from typing import Any, Iterable, Iterator, Optional, cast
class Word(ABC):
pass
@phantamanta44
phantamanta44 / keybase.md
Created June 18, 2021 01:32

Keybase proof

I hereby claim:

  • I am phantamanta44 on github.
  • I am phanta (https://keybase.io/phanta) on keybase.
  • I have a public key ASCf0eLNJ4Exee4bJQoutTmnSjPHnlI-qXy140-OyCbWAQo

To claim this, I am signing this object:

@phantamanta44
phantamanta44 / Main.hs
Created June 10, 2021 16:43
Minimal miniKanren implementation in Haskell
module Main where
import MiniKanren
-- r = n + 1
peanoSuccO :: Term -> Term -> Goal
peanoSuccO n r = r === Val (Cons n (Val Nil))
-- r = n - 1
peanoPredO :: Term -> Term -> Goal
@phantamanta44
phantamanta44 / horse_sim.py
Created December 30, 2020 20:26
from multiprocessing import Pool
from random import random
import matplotlib.pyplot as plt
import pandas as pd
from tqdm import tqdm
TIER_CNT = 4
WORKER_CNT = 8
SIM_CNT = 1_000_000
@phantamanta44
phantamanta44 / MixinEngine.java
Created July 3, 2020 18:30
package xyz.phanta.forgeveryfast.coremod.engine;
import net.minecraft.launchwrapper.IClassTransformer;
import net.minecraft.launchwrapper.LaunchClassLoader;
import org.objectweb.asm.ClassReader;
import org.objectweb.asm.ClassWriter;
import org.objectweb.asm.Handle;
import org.objectweb.asm.Opcodes;
import org.objectweb.asm.tree.*;
import xyz.phanta.forgeveryfast.coremod.engine.injector.MixinInjector;
@phantamanta44
phantamanta44 / symmetric_fizzbuzz.py
Created February 14, 2020 09:03
def cycle(elems):
mapping = { elems[i]: elems[(i + 1) % len(elems)] for i in range(len(elems)) }
return lambda e: mapping[e] if e in mapping else e
def compose(f, g):
return lambda e: f(g(e))
def cmp_list(a, b):
return all(a[i] == b[i] for i in range(len(a)))
@phantamanta44
phantamanta44 / TypeToken.java
Created August 9, 2019 19:11
/**
* Represents a parameterized type. Unfortunately necessary because the JVM doesn't support
* reified generics in all cases.
*/
@SuppressWarnings("unchecked")
public class TypeToken<T> {
/**
* The type represented by this type token.
*/