Kenny Lau
Kenny Lau
I could make use of `@P` to do the integer conversion, now a few bytes have been saved, but it would save much more bytes if we have a to/from...
http://brachylog.tryitonline.net/#code=OmVmLg&input=IlxcIg&args=Wg
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/not.20a.20structure
@ConorOBrien-Foxx Yes I do, thanks in advance.
Windows 7 32-bit Chrome 59.0.3071.115 here: 1. Confirmed. 2. No repro.
[Here](http://ideone.com/UEnCe4) is a sample program to check.
Looks like I started this issue. I also provided a [compressor](http://pyth.herokuapp.com/?code=%2B%2BhSzeSzCu%2B%2aG-hCeSzChSzHhM-RChSzCMzh0&input=aaaabbbabbbabccc&debug=0) and a [decompressor](http://pyth.herokuapp.com/?code=JC%3Ez2Kh-C%40z1ChzWJ%3D%2BYh%25tJK%3D%2F-JeYK%29sCMtM%2BRChz_Y&input=ac%03%C3%9D6%C3%B4&debug=0).
`fq2/bT[1 1 2 2 3)` should give `[1,1,2,2]`.
Why is `(` available?
Per https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/wlog.20is.20slow/near/195434556: ```lean import tactic.wlog data.rat.order lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) : (1:ℚ)/(1 - (1/a + 1/b...