GallagherCommaJack

Keybase proof

I hereby claim:

• I am gallaghercommajack on github.
• I am theseriousadult (https://keybase.io/theseriousadult) on keybase.
• I have a public key ASBBkJegFu_s7UqQ-UN1m1Ji8NHDz6fZeJI6bW0L1lERlgo

To claim this, I am signing this object:

GallagherCommaJack

data Ty : Set
data Tm : Ty → Set

postulate Var : Ty → Set

data Ty where
  pi sg : (A : Ty)(B : Var A → Ty) → Ty

data Subst {A} : (Var A → Ty) → Tm A → Ty → Set where
  -- need to fill this in

GallagherCommaJack

dashSlashSlashDelete :: (Show a, Show b, Show c) => a -> b -> c -> Routes
dashSlashSlashDelete a b c = let sa = show a
                                 sb = if length (show b) < 2 then '0':show b else show b
                                 sc = if length (show c) < 2 then '0':show c else show c
                             in gsubRoute (fold $ intersperse "-" [sa, sb, sc, ""]) (const $ fold $ intersperse "/" [sa, sb, ""])  -- gsubRoute apparently succeeds even when it should fail
                                `composeRoutes` matchRoute (fromGlob "*/*/*") idRoute -- this oughta fix that


dashSlashList :: (Show a, Show b, Show c) => [a] -> [b] -> [c] -> [Routes]
dashSlashList as bs cs = [dashSlashSlashDelete a b c | a <- as, b <- bs, c <- cs]

GallagherCommaJack

{-# OPTIONS --without-K #-}
module mini-lob where
open import Agda.Primitive public
  using    (Level; _⊔_; lzero; lsuc)
open import Data.Unit
open import Data.Product
open import Level
infixl 2 _▻_
infixl 3 _‘’_
infixr 1 _‘→’_

GallagherCommaJack

data Context : ℕ → Set
data _+c_ {n : ℕ} (Γ : Context n) : ℕ → Set
data Type : ∀ {n} → Context n → Set
data Term : ∀ {n} (Γ : Context n) → Type Γ → Set

_++_ : ∀ {n m} (Γ : Context n) → Γ +c m → Context (m + n)
_cw_ : ∀ {x n m} {Γ : Context x} (Δ : Γ +c n) → Γ +c m → (Γ ++ Δ) +c m

data Context where
  ε₀ : Context 0

GallagherCommaJack

module well-typed-syntax where
open import Data.Nat
infixl 2 _▻_
infixl 2 _▻Type_
infixl 3 _‘’_

mutual
  data Context : ℕ → Set where
    ε₀ : Context 0
    _▻_ : ∀ {n} (Γ : Context n) → Type Γ → Context (suc n)

GallagherCommaJack

# Installs agda into a folder in your home directory with sensible organization

# First, make an agda folder in the home dir
mkdir $HOME/agda

# Next, clone the repo
cd $HOME/agda
git clone https://github.com/agda/agda.git repo

cd repo

GallagherCommaJack

Ltac eq_ids :=
  repeat progress match goal with
                      [i1 : id, i2 : id |- _] => extend (eq_id_dec i1 i2)
                  end.

Lemma subst_aexp_equiv : forall i a1 a2 st,
      aeval st (subst_aexp i a2 a1) = aeval (update st i (aeval st a2)) a1.
Proof. induction a1; simpl; auto; unfold update; eq_ids; crush. Qed.

Hint Rewrite aeval_weakening subst_aexp_equiv.

GallagherCommaJack

Theorem contr_pos_eq_classic :
  (forall P Q, (~ Q -> ~ P) -> P -> Q) ->
  forall P, ~~ P -> P.
Proof. intros H P nnP. apply H with (Q := P) in nnP; intuition. Qed.

GallagherCommaJack

has_type(G,abs(V,E),arr(T1,T2)) :- has_type([[V,T1]|G],E,T2).
has_type(G,let(I,V,E),T2) :- has_type(G,V,T1), has_type([[I,T1]|G],E,T2).
has_type(G,app(E1,E2),T2) :- has_type(G,E1,arr(T1,T2)), has_type(G,E2,T1).
has_type(G,if(C,V1,V2),T) :- has_type(C,bool), has_type(G,V1,T), has_type(G,V2,T).
has_type(G,I,T) :- atom(I), append(_,[[I,T]|_],G).
has_type([],X,bool) :- X = true ; X = false.
has_type(Tm,Ty) :- has_type([],Tm,Ty).

subst(I,V,I,V).
subst(I,V,app(T1,T2),app(T12,T22)) :- subst(I,V,T1,T12), subst(I,V,T2,T22).