{{ message }}

Instantly share code, notes, and snippets.

# Brendan Zabarauskas brendanzab

Created Apr 5, 2021
Automatically generating proofs which only involve associativity of composition and adding/removing identity morphisms.
View CategorySolver.agda
 -- Yet another technique for generating proofs in Agda (in addition to the ones -- I've described in https://gist.github.com/gelisam/486d4992c0f3a3f3da2f58ff0e1a3e72): -- transform the proposition into a simpler one which can be proved using refl. -- -- This is the approach I use in my https://github.com/agda/agda-finite-prover -- package, which can prove equations universally-quantified over finite types, -- e.g. proving the commutativity of the boolean function '∧'. I simplify the -- proposition to a long enumeration of all the concrete cases, each of which -- can be proved using refl: --
Created Apr 2, 2021
View typelevel-deBruijn-scala
 object DeBruijn { sealed trait Nat sealed trait Z extends Nat sealed trait S[n <: Nat] extends Nat sealed trait Fin[n <: Nat] case class FZ[n <: Nat]() extends Fin[S[n]] case class FS[n <: Nat](n : Fin[n]) extends Fin[S[n]] val here : Fin[S[S[Z]]] = FZ()
Created Feb 27, 2021
Z3 Tutorial to Coq
View z3_tut.v
 (*| I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-coq-tutorial was trying to feed the kids their vegetables. He knew it was going to be like this from the outset and had a fun little analogy of me downhill skiing while he was about to go on a cross country slog. There are a number of factors to this. * I could use Z3's python bindings giving an air of familiarity, whereas everything was incredibly foreign in Coq. * Z3 can actually be used to declaratively state problems and automatically calculate solutions to them with very little user help, which gives it a lot more "Wow" factor. * Coq is a tool that requires significantly more background to even comprehend what the hell it is. I still think many aspects of it are tota
Last active Apr 29, 2021
View LambdaCubeIn100Lines.hs
 -- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html import Data.List (delete, union) {- HLINT ignore "Eta reduce" -} -- File mnemonics: -- env = typing environment -- vid = variable identifier in Bind or Var -- br = binder variant (Lambda or Pi) -- xyzTyp = type of xyz -- body = body of Lambda or Pi abstraction
Last active Apr 28, 2021
a pragmatic mix of de bruijn indices and levels
View IndicesAndLevels.hs
 {-# language PolyKinds #-} {-# language BlockArguments #-} {-# language AllowAmbiguousTypes #-} {-# language StrictData #-} {-# language DerivingStrategies #-} {-# language GeneralizedNewtypeDeriving #-} {-# language TypeApplications #-} {-# language BangPatterns #-} {-# language NPlusKPatterns #-} {-# language TypeFamilies #-}
Last active Nov 30, 2020
View Comp.agda
 module Comp where open import Data.List using (List; []; _∷_; _++_) open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Data.Nat using (ℕ; _+_) open import Data.List.Properties using (++-assoc; ++-identityʳ)
Last active May 4, 2021
cRAzY eSnEXt (*all* proposals mixed in)
View 2018.js
 #! Aaaaaaaaaaa this is JS!!! // https://github.com/tc39/proposal-hashbang // This file is mixing all new syntaxes in the proposal in one file without considering syntax conflict or correct runtime semantics // Enjoy!!! // Created at Nov 23, 2018 for await(const x of (new A // https://github.com/tc39/proposal-pipeline-operator |> do { // https://github.com/tc39/proposal-do-expressions case(?) { // https://github.com/tc39/proposal-pattern-matching when {val}: class {
Created Oct 31, 2020
Flat trees in ATS and C
View flat_tree.c
 /* A flat representation of * data Tree = Leaf Int | Node Tree Tree * * Either: * - *ft is LEAF and a single int follows * - *ft is NODE and two subtrees follow */ #define LEAF 0 #define NODE 1
Created Oct 23, 2020
hattifatteners.awk
View hattifatteners.awk
 #!/usr/bin/awk -f function hoop(h, w) { printf("l 0 %d ", -h); printf("c 0 -%u, %u -%u, %u 0 ", w, w, w, w); printf("l 0 %d", +h); } function hand(x, h, o, l) { printf("\n", x, h);
Last active Oct 25, 2020
A CPS interpreter for a CBV language w/ some fancy features written in syntax-rules
View syntax-rules-eval.rkt
 #lang racket ;; A CPS interpreter for a CBV language written in syntax-rules ;; e ::= 'd literal ;; | x variable ;; | (e e ...) application ;; | (λ (x ...) e) abstraction ;; | (let ((x e) ...) e) let ;; | (if e e e) conditional