Skip to content

Instantly share code, notes, and snippets.

View Myriad-Dreamin's full-sized avatar

Myriad-Dreamin

864 followers · 40 following
View GitHub Profile
@AndrasKovacs
AndrasKovacs / HIIRT.md
Last active May 9, 2025 12:13
Higher induction-induction-recursion

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.

@linhx
linhx / 1. typeorm-0.3.6-dynamic-table-name.md
Last active April 24, 2023 10:06
Working with dynamic table name with TypeOrm (test with ver 0.2.30 and 0.3.6)
@jtriley
jtriley / terminalsize.py
Created July 26, 2011 21:58
Get current terminal size on Linux, Mac, and Windows
#!/usr/bin/env python
import os
import shlex
import struct
import platform
import subprocess
def get_terminal_size():
""" getTerminalSize()