agda-stdlib VS agdarsec

For further reading, there's a paper on arity generic programming and some solutions using dependent typing in Agda.

In Rust I have never seen it. However, in Agda it's a convention, and the code looks beautifully https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Lattice/Structures.agda

Agda is a good example, as it allows you to define arbitrary Unicode-based operators and names: https://github.com/agda/agda-stdlib/blob/master/src/Data/Product.agda

Most of the times you want the first three arguments to be passed implicitly, not just the first. And the syntax for passing arguments implicitly is the same for the type argument A and the term arguments n and m. (For Agda, see e.g. l.49 here: https://github.com/agda/agda-stdlib/blob/master/src/Data/Star/Vec.agda)

I've shared my experiences, too, though I don't have specific examples. I find https://hackage.haskell.org/package/parsec-3.1.14.0/docs/src/Text.Parsec.Prim.html mush easier to read, modify, and use than https://github.com/gallais/agdarsec/blob/master/src/Text/Parser.agda . That's a specific example.