(match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))
(pp_patterns patterns)
| Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
- | Ast.LetIn (var, t1, t2) ->
- sprintf "let %s \\def %s in %s" (pp_capture_variable pp_term var) (pp_term ~pp_parens:true t1)
- (pp_term ~pp_parens:true t2)
+ | Ast.LetIn ((var,t2), t1, t3) ->
+(* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *)
+ sprintf "let %s \\def %s in %s" (pp_term var)
+(* (pp_term ~pp_parens:true t2) *)
+ (pp_term ~pp_parens:true t1)
+ (pp_term ~pp_parens:true t3)
| Ast.LetRec (kind, definitions, term) ->
let rec get_guard i = function
| [] -> (*assert false*) Ast.Implicit