Denis Buzdalov

The signature of your `match_me` looks inappropriate for the purpose, you are using it for. Why do you use `auto`-implicit argument instead of just implicit argument? `auto`-implicit arguments are such...

> https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#records doesn't show the syntax for constructing a record with non-positional arguments Right. I think it is because historically it's documented [here](https://idris2.readthedocs.io/en/latest/updates/updates.html#function-application-syntax-additions) and because record's constructor is just a...

The problems with this I see: - this `ord` implicit parameter will appear explicitly each time you have two or more sets in a signature; like, `union : SortedSet {ord}...

I realised that `%macro` annotation does not matter. In the example above its enough to have ```idris v : Unit v = %runElab extract (n : Nat ** x :...

@michaelmesser Top-level functions with `1` are cool, but inconsistent, see #818

For now the same problem is with '1.0.1' vs '1.1.0'.

Travis-CI seems to fail because of Ubuntu keyserver problems (according to [this](https://travis-ci.community/t/packages-cannot-be-authenticated-gpg-error-google-chrome-stable/3000) and [that](https://github.com/travis-ci/travis-ci/issues/9822)) :-(

Quick check shows that only the first argument's match is important: ```idris ff3 : (n, k : Nat) -> Maybe $ Y n k ff3 (S n) k = case...

> What happens if you match on, say, `Yes (Refl {x = S k})` or `Yes (Refl {x = n})`? on `Yes (Refl {x=S k})` it says `Can't match on...

> I can add this to `tests/README.md` if that's OK. I'm sure it is