Robert J. Simmons
Robert J. Simmons
I believe I needed what you describe in at least one of the Advent of Code examples. I handled it by wrapping in Javascript and writing two programs, grabbing one...
> asserting all facts from that program into the second program hmm, could the command-line API be tweaked (or used in its current form?) to achieve this effect with Unix...
Hmm... I'm guessing that the error is just an out-of-memory error as the trees got too large for the RAM allocated for that chrome tab. There's two possibilities here: -...
I will leave this open as an add-a-few-more-checks note
Corresponding branch of reference manual: https://github.com/leanprover/reference-manual/pull/587
I couldn't ultimately make the example work without UNION: ``` for movie in array_unpack($data) insert Movie { title := movie["title"], year := movie["year"], directors := assert_distinct((for dir in array_unpack(movie["directors"]) insert...
Making this a real PR, though there's no urgency of merging it until @kim-em is back in town and caught up.
I believe this is sufficiently related to not be another issue. Quick fixing the following in VSCode: ```lean theorem simpleEquality : {P Q : Prop} → P = (P ∨...
(Note: only merge after #11554)