edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-09-11 16:05:51 +03:00
Code Issues Projects Releases Wiki Activity

update 'using' regression test

Browse Source 
have implementation 'using' regression test also check for multiple named implementations
This commit is contained in:
MarcelineVQ 2020-04-22 16:53:02 -07:00
parent 4b878a8a53
commit 896cd486d1
1 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
tests/idris2/reg016/Using.idr
View File

@ -6,9 +6,16 @@ interface MagmaT a where
interface MagmaT a => SemigroupT a where
assoc: (x, y, z: a) -> (x `op` y) `op` z = x `op` (y `op` z)
[NamedMagma] MagmaT Bool where
[NamedMagma1] MagmaT Bool where
False `op` False = False
_ `op` _ = True
[NamedSemigroup] SemigroupT Bool using NamedMagma where
assoc = ?hole
[NamedMagma2] MagmaT Bool where
True `op` True = True
_ `op` _ = False
[NamedSemigroup1] SemigroupT Bool using NamedMagma1 where
assoc = ?hole1
[NamedSemigroup2] SemigroupT Bool using NamedMagma2 where
assoc = ?hole2