Add one possible variant

diff --git a/.gitignore b/.gitignore
index dfe49af29164ac756efd16ea104583c7b32aa7fe..9d204a6f80fb70d81f5f7de10a5a388e3b698aa9 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,4 @@
 *.agdai
 *~
+*#
+*#*

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index e776604da11ba805c86ac8608d84efde7a3aee49..7b75c27d479a7a4a072b78826beefd652ff7ec7b 100644 (file)
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,5 +1,6 @@
 module Typecheck where
 
+open import Data.List using ([])
 open import Data.Maybe using (Maybe; just; nothing)
 open import Function
 open import Expr
@@ -7,6 +8,9 @@ open import Type
 open import Behaviour
 open import Variable
 
+data _⊢_▸_ : Γ → Behaviour → Γ → Set where
+  t-nil : {γ : Γ} → γ ⊢ nil ▸ γ
+--  t-if-then : 
 
 typecheck_behaviour : Γ → Behaviour → Maybe Γ
 typecheck_behaviour env nil = just env