3 ms·
Idris has a replace function, and it's hard to understand and use there too. I consider its use to be a code smell, and in my experience replace expressions can
by nickdrozd 4y ago
Idris has a replace function, and it's hard to understand and use there too. I consider its use to be a code smell, and in my experience replace expressions can always be rewritten in other ways to be clearer and less verbose.
- ahelwer 4y agoThat's interesting, coming from the Lean language the analogous function - rw, or rewrite - is a real workhorse. It's often very useful to manipulate expressions when proving things. Why do you think it's a code smell?