Jonas De Vuyst
Results
3
issues of
Jonas De Vuyst
The following code ``` plusCommutativeRewrite' : (l, r : Nat) -> Fin (l + r) -> Fin (r + l) plusCommutativeRewrite' = %runElab (do rewriter {ty=`(Nat)} natPlusRefl) ``` fails with...
I thought the omission of print-and and print-or was unexpected, so I added them.