Gabriel Ebner

Uhm, that one-line change will just make it compute the transitive imports of every transitive import. My main takeaway here is that we need to go through the precompiled modules...

> The watch sometimes fails to receive notifications even if GadgetBridge indicates that it's connected. This seems to be related to the length of the notification. (P8b here.) You can...

This happened on a Samsung Galaxy S10+, is there any debugging info I can gather to help? Or any tweaks I can try out?

Today again (in two different repositories): 12/6/2021, 1:03:22 PM: ```elixir {:timeout, {GenServer, :call, [ BorsNG.GitHub, {:get_commit_status, {{:installation, 7893283}, 97922418}, {"be1210a93f23b706856a7ae6cf198f94611b4a2b"}}, 10000 ]}} ``` 12/6/2021, 1:49:45 PM: ```elixir {:timeout, {GenServer, :call,...

> Chinese text appears to be transliterated to Latin using Hanyu Pinyin. A map intended for lay readers would remove diacritics and spaces between syllables of compound words from these...

Another cool feature would be to select which "branch" of the trace tree to open by default. This would be very useful for elaboration traces where you typically have a...

#477 added the |abs| notation.

We already have (essentially) this definition, it's called `nat.partrec.code`. > Create a mapping from mu_recursive, which describes algorithms, to the functions those algorithms compute. This is the `nat.partrec.code.eval` function.

They are not equivalent, since `(·)` propagates the expected type: ```lean variable (n : Nat) #check ( (·) (n + n) : Int) -- (fun a => a) (Int.ofNat n...

We also need to translate the `⇑` and `↥` notations (in addition to the constants).