Christian Doczkal
Christian Doczkal
Now that #4 has been merged, the behaviour of the proof folding to "swallow" the (usually) blank line after the "Qed." (which was fine with the old invisible "Proof.") becomes...
The following script showcases some unfortunate notation behaviors (on the current coq.dev and finmap.dev) ```coq From mathcomp Require Import all_ssreflect finmap. Open Scope fset_scope. Lemma fsetIsep (T : choiceType) (A...
This is a draft for a tool that will queue milking/shearing orders at the closest farmer's workshop on the same z-level. In order for the tool to shear/milk an animal,...
For what its worth, here is the script I wrote to debug the equipment situation in one of my forts. Is would be nice if someone could check that the...
Those checks were recently reverse-engineered, and would be useful when directly assigning jobs to dwarves (e.g. when bypassing job bidding to make specific dwarfs carry out jobs that satisfy their...
This adds a factory for general references and uses it in the `Job` module. Similar `addGeneralRef` wrappers can probably be added to the `Unit` and `Buildings` modules.
This tool allows idle dwarfs to automatically satisfy their crafting needs. This isn't ready yet, but given that it involves quite a bit of reverse engineering and guesswork, I think...
allow immortals to satisfy their cravings for food and drink