BekaValentine

module Scratch where

postulate
  Inf  : ∀ {a} (A : Set a) → Set a
  delay : ∀ {a} {A : Set a} → A → Inf A
  force  : ∀ {a} {A : Set a} → Inf A → A

{-# BUILTIN INFINITY Inf  #-}
{-# BUILTIN SHARP    delay #-}
{-# BUILTIN FLAT     force  #-}

BekaValentine

The main judgment of this system is the hypothetical judgment

    Γ ; K ; S ⊢ M : A true

where @Γ@ is a standard type context, @K@ is a set of in-scope reset points
for the delimited continuations, and @S@ is an optional in-scope shift
indicating what the most recent shift term needs for it's hole type. @K@ and
@S@ are defined as

    K ::= e | K, k : A resets B

BekaValentine

import Control.Monad.Trans.Cont hiding (shift,reset)
import Control.Monad.Trans.Reader
import Control.Monad.Trans.State

BekaValentine

     :
     : D
     :
  A true
---------- true-proves
D proves A


D proves A
---------- :-Intro

BekaValentine

an expression with no metavars we'll call closed, and an expression w/
metavars is open

a substitution S is a for a set of metavars G is a total map from G (or any
superset of G) to closed expressions

given an open expression M with metavars in G (where G might have more than
just the ones in M), and a substitution S for G, [S]M is a closed expression

provability is a concept that applies to closed expressions, ie a closed

BekaValentine

module LE where
  
  -- These are the core types used in LE projects
  
  data Entity end
  
  data Background (e : Entity) end
  
  data Nonexistant (e : Entity) end
  

BekaValentine

newtype ChurchNat = ChurchNat { foldNat :: forall r. r -> (r -> r) -> r }

zero :: ChurchNat
zero = ChurchNat (\z _ -> z)

suc :: ChurchNat -> ChurchNat
suc n = ChurchNat (\z s -> s (foldNat n z s))

fromInt :: Int -> ChurchNat
fromInt 0 = zero

BekaValentine

data Tm : Nat -> Set where
  var : forall {n} -> Fin n -> Tm n
  lam : forall {n} -> Tm (suc n) -> Tm n
  app : forall {n} -> Tm n -> Tm n -> Tm n

BekaValentine

module Scratch where

infixr 60 _*_
infixr 50 _=>_

data Ty : Set where
  Zero One : Ty
  _*_ _=>_ : Ty → Ty → Ty

infixl 40 _,_

BekaValentine

module Scratch where


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


data Fin : Nat → Set where
  fzero : ∀ {n} → Fin (suc n)