edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-28 14:06:26 +03:00
Code Issues Projects Releases Wiki Activity
b0cad15c65
Idris2-boot/tests/idris2/basic010
History
Edwin Brady b0cad15c65 Refine dot pattern rules 
Only valid if unifying the pattern at the end doesn't solve any
metavariables. Also when elaborating applications of fromInteger etc to
constants on the LHS we need to be in expression mode, then reduce the
result later.
2019-06-27 19:16:33 +01:00
..
Comp.idr Refine dot pattern rules 2019-06-27 19:16:33 +01:00
expected Refine dot pattern rules 2019-06-27 19:16:33 +01:00
input Refine dot pattern rules 2019-06-27 19:16:33 +01:00
run Refine dot pattern rules 2019-06-27 19:16:33 +01:00