jozefg

||| The proof of the halting problem here is pretty much
||| what you would expect, we apply the standard diagonalization
||| trick to prove that if we have a halting oracle there is a
||| program which both does and doesn't terminate.

Operator dec : (0).
[dec(M)] =def= [plus(M; not(M))].

Theorem has-value-wf : [{A : base} member(has-value(A); U{i})] {
  unfold <has-value>; auto

jozefg

Operator P : (0).
[P(N)] =def= [natrec(N; unit; _._.void)].

Theorem one-not-zero : [not(=(zero; succ(zero); nat))] {
  auto;
  assert [P(succ(zero))];
  aux {
    unfold <P>; hyp-subst ← #1 [h.natrec(h; _; _._._)];
    reduce; auto
  };

jozefg

Operator Russell : ().
[Russell] =def= [{x : U{i} | not(member(x; x))}].

Tactic break-plus {
  @{ [x : _ + _ |- _] => elim <x> }
}.

Theorem u-in-u-wf : [member(member(U{i}; U{i}); U{i'})] {
  unfold <member>; eq-eq-base; unfold <bunion>; auto;
  csubst [ceq(U{i}; lam(x.snd(x)) pair(inr(<>); U{i}))]

jozefg

Operator iterate : (0; 1; 0).
[iterate(N; F; B)] =def= [natrec(N; B; _.x.so_apply(F; x))].

Operator top : ().
[top] =def= [⋂(void; _.void)].

Theorem top-is-top :
  [⋂(base; x.
   ⋂(base; y.
   =(x; y; top)))] {

jozefg

{-# OPTIONS --without-K #-}
module j-to-j where
open import Level

-- Gives rise to the annoying induction principle.
data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {a : A} → a ≡ a

-- Ignore the "Level" junk in here. It's needed because
-- we're trying to eliminate into a Set1 (U1 in Peter's

jozefg

open import Level
open import Relation.Nullary
open import Relation.Binary

module binary (ord : DecTotalOrder zero zero zero) where

A = DecTotalOrder.Carrier ord
open DecTotalOrder {{...}}

module bound where

jozefg

module general where
open import Function
import Data.Nat      as N
import Data.Fin      as F
import Data.Maybe    as M
import Relation.Nullary as R

data General (S : Set)(T : S -> Set)(X : Set) : Set where
  !!    : X -> General S T X
  _??_  : (s : S) -> (T s -> General S T X) -> General S T X

jozefg

#! /usr/bin/env python3

import os
import os.path as path
import re
import collections
from ascii_graph import Pyasciigraph
import sys

imports_re = re.compile('^import (qualified )?([a-z\.A-Z0-9]+)')

jozefg

module regex where
open import Data.Char using (Char;  _≟_)
open import Data.List using (List ; _∷_ ; [])
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty using (⊥)

-- Reason for this is because it simplifies pattern matching.
String : Set
String = List Char

jozefg

module Bracket where

data Lam = Var Int | Ap Lam Lam | Lam Lam deriving Show
data SK  = S | K | SKAp SK SK deriving Show

data SKH = Var' Int | S' | K' | SKAp' SKH SKH

-- Remove one variable
bracket :: SKH -> SKH
bracket (Var' 0) = SKAp' (SKAp' S' K') K'