Denis Buzdalov
Denis Buzdalov
`ARDUINO_LIBS` variable is calculated during configuration and it uses `LOCAL_SRCS` variable for this: https://github.com/sudar/Arduino-Makefile/blob/6f786a96b0acfb0c9b2d2f4e39911d2803088729/Arduino.mk#L974 But when `LOCAL_SRCS` contains files that are to be generated by some target in the user's...
Consider I have (accidentially or not) some `class X` which has `def main(args: Array[String]): Unit`. CBT considers this as one of the variants of possible entry points during `cbt run`...
Consider I forgot spelling of `createBuild` subcommand and I typed `cbt tools help` in a belief that it prints a list of possible subcommands. This command actually leads to printing...
Unexpected "Trying to use linear name in non-linear context" when pattern matching inside the type
# Steps to Reproduce Consider a simple dependently typed function: ```idris f1 : (n : Nat) -> Vect n Nat -> Vect (S n) Nat f1 a b = a...
# Context `%default` pragma, to my knowledge, acts from the next line till the next such pragma or till the end of file. Thus, this typechecks ```idris %default covering f...
At the moment if all alternatives of `IAlternative` with `FirstSuccess` rule are failing, only the last error is printed, which can be misleading.
# Steps to Reproduce Unified examples gist (e.g., for the future regression test) [can be found here](https://gist.github.com/buzden/454d70dfc61fbdb335eb213491b91174). Consider a primitive elaboration script that just quotates a type and logs it:...
or else they are printed together with no space and this does not look beautiful: 
This may be connected to #1690 but happens in functions, not in implementations. Names of implicit arguments are implicitly present in the scope of the function's body. Problems occur when...
Consider some definitions ```idris data X : Type someX : X data Y : Type fun : X -> (X -> Y) => Nat ``` It is important what `Y`...