Michael Fishman comments

Results 6 comments of


                                            Michael Fishman

Please persist macros with KaTeX globalGroup

I added ```json "mdmath.katexoptions": { "globalGroup": true, }, "markdown.math.enabled": false, ``` to my settings.json and reloaded vscode, but markdown still does not display the rightarrow correctly: ```latex $\newcommand{\ra}{\rightarrow}$ $\ra$ ```...

Fix: ambiguity with newly introduced divisibility symbol

Thanks! I also ran into this. Your code change fixed it for me.

Type annotations

Some thoughts: I think `State` should subclass `gym.core.ObsType`. There should possibly be other gym subclassing. Once the `unittest` PR is merged in, I may try that subclassing and see if...

Type annotations

This branch passed the existing unit tests.

recursion depth problem in chapter 7 examples

I get this error on `leanprover/lean4:v4.11.0-rc3`. Removing `add_succ` from the `simp` solves it for me. ```lean theorem zero_add_short (n : Nat) : 0 + n = n := Nat.recOn (motive...

Error "unknown identifier 'hp'" in chapter 3 "Propositions and Proofs" when using `variable (hp: p)`

@Dante3085 Thanks! I think this is the same issue. I can get the variables recognized by using `include var0 var1...` ```lean variable {p q : Prop} variable (hp : p)...