Idris2-boot/tests/idris2/reg011/mut.idr
Edwin Brady 3cf223b835 Elaborate record bodies on second mutual pass
This is the same behaviour as Idris 1. Fixes #217
2020-03-18 23:09:17 +00:00

6 lines
61 B
Idris

mutual
record A where
b : B
record B where
a : A