Brendan Zabarauskas brendanzab

A guide to ANSI on Discord

Discord is now slowly rolling out the ability to send colored messages within code blocks. It uses the ANSI color codes, so if you've tried to print colored text in your terminal or console with Python or other languages then it will be easy for you.

Quick Explanation

To be able to send a colored text, you need to use the ansi language for your code block and provide a prefix of this format before writing your text:

\u001b[{format};{color}m

Tactics in Agda

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

Glossary

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

Approachable PL Papers for Undergrads

On September 28, 2021, I asked on Twitter:

PL Twitter:

you get to recommend one published PL paper for an undergrad to read with oversight by someone experienced. the paper should be interesting, approachable, and (mostly) self-contained.

what paper do you recommend?

	(* Typechecker for MLTT with a universe hierarchy *)
	(* Build with: ocamlfind ocamlc -package angstrom,stdio -linkpkg mltt.ml -o mltt *)
	type name = string

	module AST = struct
	type tm =
	\| Var of name
	\| U of int
	\| Pi of name * ty * ty
	\| Annot of tm * ty

	type name = string

	module AST = struct
	type ty =
	\| TFun of ty * ty
	\| TNamed of string
	\| TApp of ty * ty

	type exp =
	\| Annot of exp * ty

	{-# LANGUAGE DeriveFunctor #-}
	{-# LANGUAGE DeriveGeneric #-}
	{-# LANGUAGE DerivingStrategies #-}
	{-# LANGUAGE DerivingVia #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE NoStarIsType #-}
	{-# LANGUAGE PatternSynonyms #-}


	Require Import Coq.Unicode.Utf8.

	(*
	As far as I can tell, there is way more literature in Agda on datatype-generic
	programming than in Coq. I think part of the reason is that the Agda literature
	makes liberal use of induction-recursion and fancy termination/positivity
	checking, to define fixpoints of functors. These features are not available in
	Coq.

	{-# OPTIONS --allow-exec #-}

	-- Embed a file as a string inside of an agda program.
	-- To use this, make sure to add '/bin/cat' to '~/.agda/executables'

	module Static where

	open import Function

	open import Data.Unit

	(* Compile with:
	$ ocamlfind ocamlc -package angstrom,stdio -linkpkg tychk.ml -o tychk
	Example use:
	$ ./tychk <<EOF
	> let f = (fun x -> x) : forall a. a -> a
	> in f f
	> EOF
	input : forall a. a -> a
	*)

	kind ty type.

	type tunit ty.
	type tfun ty -> ty -> ty.
	type tall (ty -> ty) -> ty.

	kind tm type.

	type unit tm.
	type app tm -> tm -> tm.