Skip to content

Instantly share code, notes, and snippets.

Daniel Gratzer jozefg

Block or report user

Report or block jozefg

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View matchless-tail.agda
module matchless-tail where
data ℕ : Set where
zero :
suc :
data Vec (A : Set) : ℕ → Set where
nil : Vec A zero
cons : {n} A Vec A n Vec A (suc n)
View wf-too-strong.agda
module wf-too-strong where
open import Data.Product using (proj₁; proj₂; _,_; _×_; Σ-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _≟_)
open import Data.Nat.Properties using (≤-antisym; ≤-refl; ≤-step)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
View nbe.ml
module Syn =
struct
type uni_level = int
type t =
| Var of int (* DeBruijn indices for variables *)
| Nat | Zero | Suc of t | NRec of t * t * t * t
| Pi of t * t | Lam of t | Ap of t * t
| Uni of uni_level
| Subst of t * subst
and subst =
View howe.agda
module howe where
open import Data.Nat
open import Data.Vec
open import Data.List
open import Data.Product
import Data.Fin as F
import Relation.Binary as B
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Relation.Nullary
View mltt.agda
module mltt where
open import Data.Nat
import Data.Fin as F
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
data Tm : ℕ → Set where
var : {n} F.Fin n Tm n
@jozefg
jozefg / exceptional.ml
Created Mar 21, 2018
Some exceptional programs in OCaml
View exceptional.ml
(* Stubs to let us pretend that OCaml is closer to our language *)
let free (x : 'a ref) = print_endline "Deallocating...."
let fork (f : unit -> 'a) : 'unit = f (); ()
(** Example 1: A finally combinator. Ensuring that a thunk is evaluated
* after another thunk regardless of the exceptions it raises
*)
let finally f g =
match f () with
| _ -> g ()
@jozefg
jozefg / intrinsic.agda
Last active Jan 12, 2018
Another formalization of "The intrinsic topology of a Martin-Lof Universe"
View intrinsic.agda
module intrinsic where
open import Function using (_∘_; id)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Sum as S
open import Data.Bool as B
open import Data.Nat as N
View configuration.ml
open Cmdliner
module type Config_t =
sig
type opt_level = O1 | O2 | O3
val int_of_opt : opt_level -> int
type config =
{ line_width : int
@jozefg
jozefg / pftools.sty
Created Oct 12, 2017
A handy package called pftools for LaTex.
View pftools.sty
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{pftools}
\@ifundefined{basedir}{%
\RequirePackage{locallabel}
}{%
\RequirePackage{\basedir locallabel}
}%
\RequirePackage{Tabbing} % Avoid the standard tabbing environment. Its \< conflicts with the semantic package.
View Unification.hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
module Unification where
import Control.Monad
import Control.Monad.Gen
import Control.Monad.Trans
import qualified Data.Map.Strict as M
import Data.Foldable
import Data.Monoid
You can’t perform that action at this time.