Skip to content

Instantly share code, notes, and snippets.

View wenkokke's full-sized avatar

Wen Kokke wenkokke

View GitHub Profile
wenkokke /
Created June 8, 2023 19:33
Build Agda to JavaScript using the GHC 9.6 JavaScript backend
set -eo pipefail
# 1. Build GHC with JavaScript backend
# 2. Get Agda source
git clone --depth=1 agda
cd agda
wenkokke /
Last active July 12, 2022 22:30
Describes the dependency graph of a Talon user directory.
from contextlib import contextmanager
from curses.ascii import isalpha
from dataclasses import dataclass
from pathlib import Path
import ast
import re
from typing import Any, Optional, Sequence, Set
wenkokke /
Last active March 2, 2024 10:32
A list of tactics for Agda…

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.


When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ :  (x y : ℤ)  x ≤ y  y ≤ x  x ≡ y
_ = solveZ3
wenkokke / .gitignore
Last active December 4, 2021 19:12 — forked from tararoys/May12knausj-master-cheatsheet.pdf
Code to print out all voice commands in the knausj talon repository,
wenkokke / Wonky.hs
Last active March 11, 2021 00:14
There's something really wonky going on with closed type families.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
module Lib where
data Nat = Z
| S Nat
-- There's something really wonky going on with closed type families: if both
wenkokke / linear.fmt
Last active February 23, 2021 17:49
Directives for formatting linear types using lhs2TeX.
%if False
% linear.fmt
% Format -> as a period when part of a lambda abstraction,
% as a lolli when used as part of a linear function arrow,
% and as an arrow otherwise.
% Wen Kokke, February 2021, version 1.0
wenkokke / lecture1.agda
Last active May 25, 2019 17:35
Slides and tutorial for my guest lectures on Agda at the University of Edinburgh in 2017.
{-(- by Wen Kokke, borrowing heavily from CS410-17 lecture 1 by Conor McBride -)-}
module lecture1 where
module sum-and-product-types where
-- so Coq and Agda are kinda the same, yet very different
-- * it's said Coq looks like ML and Agda looks like Haskell
wenkokke /
Created February 19, 2017 00:34
Convert CSV files exported from the SleepBot app to the CSV format used by toggl.
#! /usr/bin/env python3
from csv import reader, writer
from datetime import datetime, timedelta
from optparse import OptionParser
from sys import stderr
# parse command line options
parser = OptionParser()

Keybase proof

I hereby claim:

  • I am wenkokke on github.
  • I am wen ( on keybase.
  • I have a public key ASDGrBG6vQXq3xYQEocI-PSLS6yli9zR3hLMpoYidQQz2go

To claim this, I am signing this object:

wenkokke / NFA2CG.hs
Last active May 22, 2016 22:04
Convert a non-deterministic finite-state automaton (NFA) to a constraint grammar (CG) in the VislCG3 format.
{-# LANGUAGE RecordWildCards #-}
import Data.Char (toUpper)
import Data.List (intersperse)
import Text.Printf (printf)
-- |The definition of a non-deterministic finite-state automata.
-- Note: this definition assumes that all epsilon transitions
-- have been removed from the NFA.
data NFA s c = NFA