Skip to content

Instantly share code, notes, and snippets.

@zgrannan
zgrannan / Chapter3.agda
Last active November 23, 2020 08:38
Some parts of TAPL Chapter 3 Formalized in Agda
open import Data.Nat hiding (pred)
open import Data.Nat.Properties
open import Data.Nat.Induction
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation
open import Induction.WellFounded
import Relation.Binary.Construct.On as On
open ≤-Reasoning
-- Definition [Terms, Inductively] 3.2.2 (p26)
@zgrannan
zgrannan / keybase.md
Last active September 10, 2019 21:32
keybase.md

Keybase proof

I hereby claim:

  • I am zgrannan on github.
  • I am zgrannan (https://keybase.io/zgrannan) on keybase.
  • I have a public key ASB9UhLgYZ9GvNc_af9DeQ3vyGP0t_lfnr2dsH7ioMB8ywo

To claim this, I am signing this object:

@zgrannan
zgrannan / out
Created September 19, 2017 09:27
Sending build context to Docker daemon 3.072kB
Step 1/4 : FROM postgres:9.6
---> 1227c4263c8c
Step 2/4 : MAINTAINER Chia-liang Kao <clkao@clkao.org>
---> Running in 33a9b9962d33
---> e0db71bde68f
Removing intermediate container 33a9b9962d33
Step 3/4 : ENV PLV8_VERSION v1.5.3 PLV8_SHASUM "fac8052c926c9ece74f655500caeca50552c0c4b4c7081c0c7946e06ed114d1c v1.5.3.tar.gz"
---> Running in 4477b35d697d
---> f6f3d3c88587
package com.github.tminglei.slickpg
import org.postgresql.util.HStoreConverter
import org.scalatest.FunSuite
import slick.jdbc.{GetResult, PositionedResult, PostgresProfile}
import scala.collection.convert.{WrapAsJava, WrapAsScala}
import java.sql.Timestamp
import java.text.SimpleDateFormat
package com.github.tminglei.slickpg
import org.postgresql.util.HStoreConverter
import org.scalatest.FunSuite
import slick.jdbc.{GetResult, PositionedResult, PostgresProfile}
import scala.collection.convert.{WrapAsJava, WrapAsScala}
import java.sql.Timestamp
import java.text.SimpleDateFormat

Keybase proof

I hereby claim:

  • I am zgrannan on github.
  • I am zackg (https://keybase.io/zackg) on keybase.
  • I have a public key whose fingerprint is FB4F 6641 1B75 439C 492F 9163 2697 DD20 4B2E C103

To claim this, I am signing this object: