larrytheliquid

open import Data.Empty using ( ⊥ ; ⊥-elim )
open import Data.Unit using ( ⊤ ; tt )
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
  renaming ( _≟_ to _≟B_ )
open import Data.Nat using ( ℕ ; zero ; suc )
    renaming ( _≟_ to _≟ℕ_ )
open import Data.Product using ( Σ ; _,_ )
open import Relation.Nullary using ( Dec ; yes ; no )
open import Relation.Binary using ( Decidable )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

larrytheliquid

λ A m n →
  ind
  (`Arg (Tag ("nil" ∷ "cons" ∷ []))
   (λ t →
      case
      (λ _ →
         Desc
         (μ
          (`Arg (Tag ("zero" ∷ "suc" ∷ []))
           (λ t₁ → case (λ _ → Desc ⊤) (`End tt , `Rec tt (`End tt) , tt) t₁))

larrytheliquid

open import Data.Bool
open import Data.Nat
module HypotheticalFunMatching where

{-
Imagine that the expressions in the pattern positions are first evaluated to values/neutrals.
So for example, "not" really becomes elimBool and "_+_" becomes two nested elimℕ's.

A wildcard match is always necessary because there are infinitely many intentionally different
functions.

larrytheliquid

{-
How does local completeness (http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/03-harmony.pdf) generalize to eliminators?

Below is the eliminator for `ℕ` that does not include the inductive hypothesis `P n` in the `suc n` branch.
It still passes local completeness because the `suc n` branch still includes the `n` index, it merely omits the inductive hypothesis.

Caveats:
1. `ℕ` is a datatype rather than a standard logical proposition, and it has many proofs/inhabitants for the same type.
2. I'm being more strict here by requiring the expansion to equal the input, rather than merely proving the same proposition.
-}

larrytheliquid

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

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

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 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 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

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