- return_term loc (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2))
+ return_term loc
+ (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2))
b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
typ = OPT [ SYMBOL ":"; t = term -> t ];
SYMBOL "."; body = term ->
let binder =
List.fold_right
b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
typ = OPT [ SYMBOL ":"; t = term -> t ];
SYMBOL "."; body = term ->
let binder =
List.fold_right
- (fun var body -> CicTextualParser2Ast.Binder (b, Cic.Name var, typ, body))
+ (fun var body ->
+ let name =
+ match var with
+ | "_" -> Cic.Anonymous
+ | var -> Cic.Name var
+ in
+ CicTextualParser2Ast.Binder (b, name, typ, body))
| LPAREN "("; head = term; args = LIST1 term; RPAREN ")" ->
return_term loc (CicTextualParser2Ast.Appl (head :: args))
| i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, 0))
| LPAREN "("; head = term; args = LIST1 term; RPAREN ")" ->
return_term loc (CicTextualParser2Ast.Appl (head :: args))
| i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, 0))