LARA

Inserting declaration into Gamma
================================

For each method

def m[A](x_1:T_1, ..., x_n:T_n) : T = { ... }

we insert into Gamma the pair:

 (m,\forall A. T_1 x ... T_n -> T)

Method call rule for a single type parameter
============================================


 (m,\forall A. T_1 x ... T_n -> T) in Gamma
 Gamma |- e_i : S_i
 S_i = T_i[A:=T0]
 S = T[A:=T0]
-------------------------------------------
    Gamma |- m[T0](e_1,...,e_n) : S


Type checking method body
=========================

For method

def m[A](x_1:T_1, ..., x_n:T_n) : T = e 

we check that

Gamma + { (x_1,T_1),...,(x_n,T_n)}  |- e : T

In other words, the type checking rule remains the same as
without generic types, but now the type variables such as A
may occur as types in the environment.