Oct 21, 2026, 1:16 AMIf this were scheme or ocaml I'm pretty sure I could do what i'm doing with zip or other pointfree combinators but unfortunately Idris's most Haskell-like quality is the documentation believes that giving the type of a function is sufficient for a reader to understand what it is the arguments do
Oct 21, 2026, 1:55 PMCurrently drowning in a never-ending chain of writing basic "case" or "if" statements and getting unintelligible errors like "expected =>" on a => or "expected end of expression". Trying to not run to Mastodon for help on every one. Did encounter one thing that seems so actionable I'm considering filing it:
Why are members of the sequence "0..7" not Fin 8?
![let new = for [0..7] (\i => shiftL (the Bits64 1) (cast i))
"cast i" is highlighted saying that i (0..7) is an integer and "cast i" needs a Fin 64](https://files.mastodon.social/media_attachments/files/117/479/226/319/701/575/original/3558a17cd05a3caf.png)
@mcc because i doesn't know anything about what list was given, all it knows is that it's an Integer
you probably want
allFins 8 for all the numbers in Fin 8iterateN to apply (fun x => shiftL x FZ) on l eight times and collect the intermediate results in a list