{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":78,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":76,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":78,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":76,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":82,"severity":"information","text":"test\n"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":67,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":78,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":76,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"rb_map_ts.lean","pos_col":2,"pos_line":82,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":90,"file_name":"rb_map_ts.lean","pos_col":0,"pos_line":90,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":68}
{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":72}
{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\n2 goals\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":86}
