Mac Malone
Mac Malone
> -v to what? Sorry, `lake build` (e.g., `lake build -v`).
> One tricky part is this case - > > ```haskell > example = foo & (#bar . #baz) .~ 'z' > ``` This is not valid syntax with `UnboxedTuples`...
awaiting-review
awaiting-review
@fgdorais From my view, that seems like a Batteries maintainer question. I addressed the review comments, so the next step was to hear back whether my response / changes were...
I imagine this is a problem with other commands as well? All of them just mention the missing required argument. Perhaps Lake should print out the help page (e.g., `lake...
I think one confounding issue here is that, like Python it is not necessarily ideal to have users importing their whole package into a top-level module. Ideally, downstream users are...
Now that we have position termination proofs in core (e.g., `termination_by text.utf8ByteSize - pos.byteIdx`), it may be worth supporting these automatically through `decreasing_trivial`. For example, I did this over in...
@semorrison While I do agree that I (probably mistakenly) lean towards experts, my concern here was one focused on beginners. We do not want to habituate them into catch-all roots....
@semorrison The French quotes in the imports can probably be removed because Lean does not parse keywords in import statements. In the Lake configuration file, however, it is not possible...