Lîm Tsú-thuàn dannypsnl
yangzhixuan
/ EasierIndices.agda
Created
September 28, 2025 13:47
Making working with de Brujin indices easier
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {- | |
| This file demonstrates a technique for making working with de Bruijn-indexed | |
| terms easier that I learnt from the paper /The Linearity Monad/ by Jennifer | |
| Paykin and Steve Zdancewic. After defining well-typed terms `Γ ⊢ τ` using de Bruijn | |
| indices, we define an auxiliary function `lam` that takes in the variable term explicitly: | |
| > lam : {V : Type} {Γ : Cxt V} {τ σ : Ty V} | |
| > → (({Δ : Cxt V} → {{IsExt Δ (Γ , τ)}} → Δ ⊢ τ) | |
| > → (Γ , τ) ⊢ σ) | |
| > → Γ ⊢ τ ⇒ σ |
bobatkey
/ tuple.agda
Created
February 27, 2024 10:08
"A Quick Introduction to Denotational Semantics using Agda" notes for talk given at TUPLE 2024 (https://typesig.comp-soc.com/tuple/)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --postfix-projections #-} | |
| module tuple where | |
| ------------------------------------------------------------------------------ | |
| -- |
AndrasKovacs
/ NbEUnitEta.hs
Last active
August 5, 2024 15:57
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# language | |
| BlockArguments | |
| , ConstraintKinds | |
| , ImplicitParams | |
| , LambdaCase | |
| , OverloadedStrings | |
| , PatternSynonyms | |
| , Strict | |
| , UnicodeSyntax | |
| #-} |
MaxwellDupre
/ trim-generations.sh
Last active
December 21, 2025 15:41
— forked from Bondrake/trim-generations.sh
NixOS script to keep 30 generations or 30 days, whichever is greater (configurable, profile is selectable)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/usr/bin/env bash | |
| set -euo pipefail | |
| ## Defaults | |
| keepGensDef=30; keepDaysDef=30 | |
| keepGens=$keepGensDef; keepDays=$keepDaysDef | |
| ## Usage | |
| usage () { | |
| printf "Usage:\n\t ./trim-generations.sh <keep-gernerations> <keep-days> <profile> \n\n |
neel-krishnaswami
/ pcomb.ml
Last active
September 14, 2025 09:26
A linear-time parser combinator library in Ocaml
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module C : sig | |
| type t | |
| val empty : t | |
| val one : char -> t | |
| val union : t -> t -> t | |
| val inter : t -> t -> t | |
| val top : t | |
| val mem : char -> t -> bool | |
| val make : (char -> bool) -> t | |
| val equal : t -> t -> bool |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --cubical #-} | |
| module natmod where | |
| open import Cubical.Foundations.Prelude | |
| data Ctx : Type | |
| data _⊢_ : Ctx → Ctx → Type | |
| data Ty : Ctx → Type | |
| data Tm : Ctx → Type | |
| -- This is halfway between EAT and GAT. | |
| -- GAT is hard! Why is EAT so easy? |
Trebor-Huang
/ freeCCC.agda
Last active
August 12, 2025 08:46
Defines STLC as the free CCC over the base type in Agda directly with HITs. Proves canonicity directly by induction.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --cubical --no-import-sorts --postfix-projections -W ignore #-} | |
| module freeCCC where | |
| open import Cubical.Foundations.Prelude | |
| open import Cubical.Foundations.HLevels | |
| open import Cubical.Foundations.Function | |
| open import Cubical.Foundations.Isomorphism | |
| open import Cubical.Data.Unit using (Unit; isPropUnit; isSetUnit) | |
| open import Cubical.Data.Bool using (Bool; true; false; if_then_else_; isSetBool) | |
| open import Cubical.Data.Sum using (_⊎_; inr; inl) | |
| open import Cubical.Data.Sigma using (Σ; _×_; ΣPathP) |
typeswitch-dev
/ daiyon.c
Last active
January 2, 2026 17:03
第四 (Daiyon) — a Japanese & Forth inspired postfix language
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #include <stdio.h> | |
| #include <string.h> | |
| #include <assert.h> | |
| FILE *in; long M[1<<24]={0}, *D, *R, H=0x130000, IP=0, T; | |
| long getu() { long t, h = getc(in); if (h < 0xC0) return h; | |
| t = ((h&0x1F) << 6) | (getc(in) & 0x3F); if (h < 0xE0) return t; | |
| t = ( t << 6) | (getc(in) & 0x3F); if (h < 0xF0) return t; | |
| t = ( t << 6) | (getc(in) & 0x3F); return t & 0x1FFFFF; } | |
| void putu(long c) { if (c < 0x80) { putchar(c); return; } | |
| if (c < 0x7FF) { putchar(0xC0|(c>>6)); } else { |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# language LambdaCase, Strict, BangPatterns, ViewPatterns, OverloadedStrings #-} | |
| {-# options_ghc -Wincomplete-patterns #-} | |
| module UnivPoly where | |
| import Data.Foldable | |
| import Data.Maybe | |
| import Data.String | |
| import Debug.Trace |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ;; Exporting free identifier table operations that close over a global map | |
| #lang racket/base | |
| (require racket/list | |
| syntax/id-table) | |
| (provide env-ref env-has-id? env-add!) | |
| (define id-table (make-free-id-table)) |
NewerOlder