{"msgs":[{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n  trace\n  tactic.trace\nAdditional information:\ninfo_id_pre_elab.lean:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n  trace\n  tactic.trace\nAdditional information:\ninfo_id_pre_elab.lean:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n  trace\n  tactic.trace\nAdditional information:\ninfo_id_pre_elab.lean:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"info_id_pre_elab.lean","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"check result","end_pos_col":27,"end_pos_line":7,"file_name":"info_id_pre_elab.lean","pos_col":0,"pos_line":6,"severity":"information","text":"λ (tac : tactic unit), (abstract tac none) : tactic unit → tactic unit"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"response":"ok","seq_num":4}
{"record":{"full-id":"tactic.abstract","source":,"type":"tactic unit → opt_param (option name) none → opt_param bool tt → tactic unit"},"response":"ok","seq_num":7}
