mietek

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}

import Data.String (IsString, fromString)
import GHC.TypeLits (KnownSymbol, Symbol, someSymbolVal, symbolVal)

mietek

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}


-- Naturals.

data Nat :: * where
  Zero :: Nat

mietek

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

data Nat :: * where
  Zero :: Nat
  Suc  :: Nat -> Nat

instance Eq Nat where
  Zero  == Zero   = True
  Suc n == Suc n' = n == n'

mietek

{-# LANGUAGE ScopedTypeVariables #-}

data Zero
data Suc n
  
type One   = Suc Zero
type Two   = Suc One
type Three = Suc Two

class Nat n where

mietek

module BasicIPC.Syntax.GentzenNormalForm3 where

open import BasicIPC.Syntax.GentzenNormalForm public


data Re {Γ} : ∀ {A} → Γ ⊢ A → Γ ⊢ A → Set where
  conglamʳᵉ  : ∀ {A B} {t t′ : Γ , A ⊢ B} →
               Re t t′ → Re (lam t) (lam t′)

  congappʳᵉ  : ∀ {A B} {t t′ : Γ ⊢ A ▻ B} {u u′ : Γ ⊢ A} →

mietek

module BasicIPC.Syntax.GentzenWithProofTerms where

open import BasicIPC.Syntax.Common public


data Tm : Set where
  VAR  : Atom → Tm
  LAM  : Atom → Tm → Tm
  APP  : Tm → Tm → Tm
  PAIR : Tm → Tm → Tm

mietek

module Intuition where

open import Data.Empty using (⊥)
open import Data.Product using (_,_ ; proj₁ ; proj₂) renaming (_×_ to _∧_)
open import Data.Sum using (inj₁ ; inj₂) renaming (_⊎_ to _∨_)
open import Relation.Nullary using (¬_)

foo : ∀ {a} {A : Set a} → ¬ ¬ (A ∨ ¬ A)
foo x = x (inj₂ (λ y → x (inj₁ y)))

mietek

module BasicIPC.Syntax.GentzenNormalForm2 where

open import BasicIPC.Syntax.GentzenNormalForm public


data NfNe⁼ {A Γ} (t : Γ ⊢ A) : Set where
  nfⁿᶠⁿᵉ⁼ : (t′ : Γ ⊢ⁿᶠ A) → {{_ : nf→tm t′ ≡ t}} → NfNe⁼ t
  neⁿᶠⁿᵉ⁼ : (t′ : Γ ⊢ⁿᵉ A) → {{_ : ne→tm t′ ≡ t}} → NfNe⁼ t

mietek

module Experiments where

open import BasicIS4.Syntax.DyadicGentzen public


-- A strict total order on types.

mutual
  infix 3 _<ᵀˣᵀ_
  _<ᵀˣᵀ_ : Ty × Ty → Ty × Ty → Set

mietek

{-

Nordström, B. (1988) “Terminating general recursion”
http://dx.doi.org/10.1007/BF01941137

Mu, S-C. (2008) “Well-founded recursion and accessibility”
http://www.iis.sinica.edu.tw/~scm/2008/well-founded-recursion-and-accessibility/

-}