Formalise checked annotated lambdas
The implementation of the LIGO type checker permits the following typing rule:
| E_lambda lambda, T_arrow { type1 = arg_type; type2 = ret_type } ->
let ctx, lambda =
check_lambda ~raise ~loc ~options ~ctx lambda arg_type ret_type
in
( ctx
, let%bind lambda = lambda in
return @@ E_lambda lambda )
This is used to handle checking judgements of the form: \Gamma |- fun (x : A) -> e <= B -> C