ionathanch / graphite

A data visualization library for Racket.

_{^{closure ahead}}

Frankly everything you need to know about me should already be in the sidebar. Here, have some Agda instead:

{-# OPTIONS --sized-types #-}
open import Size
open import Data.Empty

data _<_ : Size → Size → Set where
  lt : ∀ s → (r : Size< s) → r < s

data Acc (s : Size) : Set where
  acc : (∀ {r} → r < s → Acc r) → Acc s

false₁ : ⊥
false₁ = ¬wf∞ (wf ∞) where
  wf : ∀ s → Acc s
  wf s = acc (λ {(lt .s r) → wf r})
  ¬wf∞ : Acc ∞ → ⊥
  ¬wf∞ (acc p) = ¬wf∞ (p (lt ∞ ∞))

Oh? You want more? Here's more:

data _≡_ : Size → Size → Set where
  refl : ∀ {i} → i ≡ i

data Up! : Size → Set where
  huh : ∀ {i} → Up! i
  up! : ∀ {i} → {j : Size< i} → Up! j → Up! i

false₂ : ⊥
false₂ = hup! ∞ refl huh where
  hup! : ∀ i → i ≡ (↑ ∞) → Up! i → ⊥
  hup! .∞ refl u = hup! ∞ refl (up! u)