larrytheliquid

tex = ARGV[0]
modified_at = File.mtime tex
puts "Starting from: #{modified_at}"

loop do
  if modified_at != (mtime = File.mtime tex)
    modified_at = mtime
    `pdflatex #{tex}`
    puts "Recompiled for: #{modified_at}"
  end

larrytheliquid

module Maths where

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

plus : Nat → Nat → Nat
plus zero n = n
plus (suc m) n = suc (plus m n)

larrytheliquid

(defvar slide-delimiter
  "----------------------------------------------------------------------"
  "Delimiter used for changing slides")

(defun narrow-to-slide ()
  (interactive)
  (search-forward slide-delimiter)
  (next-line)
  (let ((start (point)))
    (search-forward slide-delimiter)

larrytheliquid

(set-fontset-font t '(#x2080 . #x00208e) "Monoco")
(set-fontset-font t '(#x002070 . #x00207e) "Monoco")

larrytheliquid

module IRDTT where
open import Level
open import Data.Product public using ( Σ ; _,_ ; proj₁ ; proj₂ )
open import Data.Sum public using ( _⊎_ ; inj₁ ; inj₂ )

record ⊤ {a} : Set a where
  constructor tt

data Type {a} : Set (suc a)
⟦_⟧ : ∀{a} → Type {a} → Set a

larrytheliquid

module IRDTT where
open import Level
open import Data.Product using ( _,_ )
  renaming ( Σ to Sigma ; proj₁ to proj1 ; proj₂ to proj2  )
open import Data.Sum
  renaming ( _⊎_ to Sum ; inj₁ to inj1 ; inj₂ to inj2 )

record Unit {a} : Set a where
  constructor tt

larrytheliquid

open import Level
open import Data.Product public using ( Σ ; _,_ ; proj₁ ; proj₂ )

data ⊥ {a} : Set a where

! : ∀ {a b} {A : Set a} → ⊥ {b} → A
! ()

record ⊤ {a} : Set a where
  constructor tt

larrytheliquid

module TrailEquality where
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality

data Maybe (A : Set) : Set where
  just : (x : A) → Maybe A
  nothing : Maybe A

data ℕ : Set where
  zero : ℕ

larrytheliquid

open import Data.Bool
open import Data.Nat
open import Data.String
module CrazyNames where

data U : Set where
  `Bool `ℕ : U

El : U → Set
El `Bool = Bool

larrytheliquid

airtheliquid:spire larrytheliquid$ ./spire 
Enter type: 
If (Not (Not True)) Bool Unit
Enter term: 
Not True
Well typed!
=> False : Bool