10:00:35	 From  Mark Lavrentyev : Welcome!
10:06:02	 From  Christopher Wolfram : void* never lies
10:06:35	 From  Ryan Greenblatt : The good ole reinterpret_cast
10:06:43	 From  Gene Siriviboon : Sometime when you import program incorrectly you can have type overloading
10:06:52	 From  Thomas Del Vecchio : I mean your sumTo function was “Number -> Number”, but if you gave it a negative or non-integer value, it would have broken?
10:06:53	 From  Mary Loukidi-Papanikoli : Or plain old inheritance
10:07:10	 From  Mary Loukidi-Papanikoli : (not really a lie, but...)
10:07:38	 From  Christopher Wolfram : I used a language where the function for sqrt returns floats when given numbers greater than 0 and complexes for numbers less than 0, and it ha a whole system for have types that also have prerdicates like whether they are positive
10:10:29	 From  Gene Siriviboon : Validity?
10:10:41	 From  Gene Siriviboon : Like we want to deduct a theorem from a threorem
10:11:00	 From  Ben Ryjikov : If you want to prove something about integers, you need to use rules that apply to integers
10:11:00	 From  Thomas Del Vecchio : The type might be the outer most operator?
10:11:05	 From  Daniel Kostovetsky : Would it depend on the kind of proof?
10:11:12	 From  Christopher Wolfram : Well you could have sentences as a composite type made up of other sentences, and you could have letters which are a special kind of sentences, but that doesn’t sound very exciting
10:11:23	 From  Justin Sanders : I guess like if you show something for all integers or all complex numbers those are kinda types
10:11:34	 From  Daniel Kostovetsky : e.g. [statements] -> [other statements]
10:11:43	 From  Daniel Kostovetsky : [statements] -> [tautology]
10:11:50	 From  Daniel Kostovetsky : [statements] -> [contradiction]
10:14:07	 From  Justin Sanders : induction does infinite program steps
10:14:48	 From  Christopher Wolfram : It seems like you would take an induction axiom^
10:14:50	 From  Mark Lavrentyev : https://jscoq.github.io/node_modules/jscoq/examples/scratchpad.html
10:16:36	 From  Jiahao Yuan : excuse me, can you make the code bigger? thanks
10:16:43	 From  Jiahao Yuan : yes
10:19:14	 From  Christopher Wolfram : how did you type  the forall symbol?
10:19:41	 From  Mark Lavrentyev : In the online editor  you can type `forall` and it'll do the same thing :)
10:21:45	 From  Christopher Wolfram : Could you explain what destruct does again?
10:22:14	 From  Christopher Wolfram : Ah ok
10:22:34	 From  Christopher Wolfram : and is there a list of theorems like "reflexivity"
10:24:52	 From  Daniel Kostovetsky : “The only thing we have to true is truth itself”
10:27:19	 From  Thomas Del Vecchio : Is H just a keyword?
10:27:28	 From  Daniel Kostovetsky : But how does destruct H prove 0=1?
10:28:08	 From  Christopher Wolfram : Why the label “H”?
10:28:18	 From  Mark Lavrentyev : H for hypothesis
10:32:39	 From  Daniel Kostovetsky : Why is it like “left: A -> either
10:32:52	 From  Daniel Kostovetsky : And not left: A
10:33:01	 From  Christopher Wolfram : Left is a case for either that takes an A and returns an either.
10:33:22	 From  Monica Roy : is there any other way syntactically to take in multiple arguments in the cases? or does it always have to be arg1 -> arg2 -> …
10:34:13	 From  Christopher Wolfram : That’s kind of ugly though because we never refer to “a”  and “b”
10:34:45	 From  Daniel Kostovetsky : or
10:36:54	 From  Christopher Wolfram : It doesn’t look like it takes 4 arguments….
10:38:27	 From  Christopher Wolfram : So Example is basically for constructive proofs?
10:39:30	 From  Christopher Wolfram : Oh so the parsers does not care at all? Its’ just for the humans?
10:39:40	 From  Monica Roy : sorry could you explain how you got to the last line of the proof, again?
10:39:52	 From  Monica Roy : yeah
10:41:14	 From  Monica Roy : thanks!
10:41:57	 From  Christopher Wolfram : Can you make the text bigger again?
10:47:40	 From  Christopher Wolfram : (Why do the line numbers count down?!)