repos / jolie.agda.git

commit

da9b32f

parent

c5f6d3d

author

Eugene Akentyev

date

2016-10-23 00:07:35 +0400 +04

Add one possible variant

1@@ -1,2 +1,4 @@
2 *.agdai
3 *~
4+*#
5+*#*

 1@@ -1,5 +1,6 @@
 2 module Typecheck where
 3 
 4+open import Data.List using ([])
 5 open import Data.Maybe using (Maybe; just; nothing)
 6 open import Function
 7 open import Expr
 8@@ -7,6 +8,9 @@ open import Type
 9 open import Behaviour
10 open import Variable
11 
12+data _⊢_▸_ : Γ → Behaviour → Γ → Set where
13+  t-nil : {γ : Γ} → γ ⊢ nil ▸ γ
14+--  t-if-then : 
15 
16 typecheck_behaviour : Γ → Behaviour → Maybe Γ
17 typecheck_behaviour env nil = just env