iacore
# Attempt 2 ``` match_me : f t -> Eff [f] t match_me x = MkEff x ans : Eff [Foo] () ans = do let interim = match_me MkFoo...
maybe Idris cannot unify higher-ordered type like `Foo Nat`?
Sorry, typo. *Attempt 2* still produce the same error.
Is there a work around? It seem to be one fundamental behavior of Idris.
Should I close this issue? Or maybe the error message could be better? This behaviour stopped me from making `do` notation more flexible: https://github.com/locriacyber/idris2-eff/blob/0403d8128b0b1fa21cb315dc0d99bbd9239a8ff0/src/Control/Eff/Sugar.idr#L10-L13 https://github.com/locriacyber/idris2-eff/blob/0403d8128b0b1fa21cb315dc0d99bbd9239a8ff0/src/Test/Sugar.idr
The problem is not about modulo. The problem is using `r` (global variable) without `let`.
@stefan-hoeck don't use `%` at all. ~~The terrible language doesn't have `%` for BigInt.~~ https://tc39.es/ecma262/multipage/ecmascript-language-expressions.html#sec-applystringornumericbinaryoperator Edit: I found it later in spec https://tc39.es/ecma262/multipage/ecmascript-data-types-and-values.html#sec-numeric-types
We can, probably. It works in Node.JS and Firefox for me. It's the ECMA standard for ~~JS~~ ECMAScript 2023 that's self-inconsistent.
> Anyway, implementations with orderings in a signature should have variants which take sets with different orderings and produces a set with, say, an ordering of the left one, just...
Is it a good idea to change `Lazy a` to `() -> a` and add syntax magic on it? Totality checker seem to work. ``` data LazyList : Type ->...