on 293c8a2 help sign in
Idris-dev/lib/Language
1 folder, 1 file
../ Reflection/Formatting improvements Reflection.idrAllow 'rewrite ... in' to assert the resulting type "rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings.