Steve Dunham

I can do small bits of fixing here and there, but I am not actually using it at all. And I agree with stefan that it would best be maintained...

The startup script for idris looks like: ``` #!/bin/sh # @generated by Idris 0.7.0-fc3d2a04d, Chez backend set -e # exit on any error if [ "$(uname)" = Darwin ]; then...

That code in the Parser is working for multiline single quoted strings. You can see it in action here: ```idris foo = "dfasd asdfasd" ``` returns: ``` Error: Multi-line string...

Thanks for the bug report. This is not related to the `>>`, any continuation line of a function clause has to be indented more than the current indentation level (just...

To unblock you: It is not pretty, but explicitly matching the implicit argument of the `MkDPair` works around the issue: ```idris evaluate : (e : Expr) -> (Checks e t)...

I had added some additional logging and the "Patterns for fail require matching on different types" was referring to the argument filled in for `MkDPair` (which it named `e`) and...

At first I thought it was shadowing, but the two `n` are being treated as the same before it gets to the RHS. ```idris foo : (n : Nat) ->...

On Idris2 0.8.0 and the code posted above, I get an error: ``` 1/1: Building Algebra.Field (src/Algebra/Field.idr) Error: While processing right hand side of zero_is_absorbent. Can't solve constraint between: zero...

Here is a version with the `parameters` desugared. I wanted to double check there wasn't a `parameters` bug involved here: ```idris import Data.Fin %default total foo : (0 bang :...

It seems like it could be exponential if we start recursing on these arguments, unless we've got some heuristics to help (e.g. return "don't know" if there are multiple candidates...