Agda goes above and beyond that when you consider their mix-fix syntax… While it might not be perfect, it’s a hella lot closer to mathematical proving/programming with normal functional programming “constructs” (for lack of a better word… idris etc, also the struggle with sized types)