Builtin now takes two arguments: function_name and function_type
Changes to be committed: * btl/types.typer: reflect "Builtin" change * src/elexp.ml: unsusp susp * src/REPL.ml: - reflected change linked to elexp.ml - file reading is now done with eval_file * src/builtin.ml - add predefined_table and get_predefine * src/lparse.ml: - simplified handle_call as it had a lot of legacy code - constructor now inherit inductive's formal_args as Aerasable arguments cons : (a : Type) ≡> (v : a) -> List a -> List - predef_table is populated in default_ctx right after builtin type definition were read * src/debug_util.ml: - added: -typecheck argument
Loading
Please register or sign in to comment