Skip to content

Instantly share code, notes, and snippets.

Avatar

Brendan Zabarauskas brendanzab

View GitHub Profile
@andrejbauer
andrejbauer / Corey.agda
Created Jun 1, 2021
The type of bit streams is uncountable.
View Corey.agda
open import Data.Bool
open import Data.Empty
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality
module Corey where
-- streams of bits
record Stream : Set where
@AndrasKovacs
AndrasKovacs / UnivPoly.hs
Last active Jun 14, 2021
simple universe polymorphism
View UnivPoly.hs
{-# 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
@hwayne
hwayne / acct.py
Created May 21, 2021
Example of a use case for inheritance
View acct.py
class Bank:
def __init__(self, balance):
assert balance > 0
self.balance = balance
def deposit(self, val):
self.balance += val
def withdraw(self, val):
if val <= self.balance:
View warned.ml
(*
e -> true | false
| 0 | 1 | 2 | …
| id
| e + e | e - e | e && e | e || e
| if e then e else e
t -> bool | int
@gelisam
gelisam / CategorySolver.agda
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:
--
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()
@philzook58
philzook58 / z3_tut.v
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
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
@ekmett
ekmett / IndicesAndLevels.hs
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 #-}
@Boarders
Boarders / Comp.agda
Last active Nov 30, 2020
compiler correctness for addition language
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ʳ)