Hanting Zhang
Hanting Zhang
This PR implements `fin_cases` from mathlib3. It largely follows the original idea behind Scott's code. There are a few notable details for this PR - To have `fin_cases`s full functionality,...
Note: I'm raising this issue mostly for bookkeeping purposes -- if someone wants to address them please feel free to! (Anyways, I'm probably going to come back and add these...
We prove the Zassenhaus/butterfly lemma. Hooray! --- (I didn't really know where to put this. It doesn't feel like it deserves its own file, but it isn't quite an isomorphism...
We define a new structure `decomposition ι R M` as the type of `ι`-indexed decompositions of `M`. We provide a correspondence between internal direct sums and decompositions. Some helpful auxiliary...
Due to upstream changes https://github.com/lurk-lab/arecibo/pull/285 https://github.com/lurk-lab/arecibo/pull/288
Copy pasted from [notion design doc](https://www.notion.so/lurk-lab/Cache-and-Public-Parameters-4f79ecbc861f43059b806ae7bdc2e401): - Remove `MemCache` and `DiskCache` in favor of `FileMap` and `FileStore` in `fcomm`. - Refactor the whole `public_parameters` directory. - For every cached type...
Depends on - https://github.com/lurk-lab/arecibo/issues/69 - https://github.com/lurk-lab/arecibo/issues/67 - https://github.com/lurk-lab/lurk-rs/issues/746 After these 3, it should be very natural to merge the instance API into the logic of `FileMap`, and we get a...
From: https://zulip.lurk-lab.com/#narrow/stream/47-systems/topic/Coprocessors.20.2B.20NIVC/near/106928 I've started working on the benchmarking metrics and am running into a strange bug. In my branch here (https://github.com/lurk-lab/lurk-rs/compare/coproc-benchmarks), I tried to modify the sha256 example to handle...
I have the following error: ``` Lurk REPL welcomes you. > "}" Mismatched brackets: '}' is unpaired > "\} " Mismatched brackets: '}' is unpaired ``` Also happens with `()`...