From da9b32f2ad22cde071e15c9abbf2ef89c12b25a8 Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Sat, 22 Oct 2016 23:07:35 +0300
Subject: [PATCH] Add one possible variant

---
 .gitignore         | 2 ++
 src/Typecheck.agda | 4 ++++
 2 files changed, 6 insertions(+)

diff --git a/.gitignore b/.gitignore
index dfe49af..9d204a6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,4 @@
 *.agdai
 *~
+*#
+*#*
diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index e776604..7b75c27 100644
--- 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
-- 
2.50.1