idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Add two cases to the record projection test.

Browse Source
This commit is contained in:
Matus Tejiscak 2020-09-11 00:29:14 +02:00
parent ba89bbcc0d
commit 9652179990
1 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
tests/idris2/record004/Main.idr
View File

@ -75,3 +75,14 @@ rect =
-- user-defined projections work, too (should they?)
(.squared) : Double -> Double
(.squared) x = x * x
-- #649: Forced patterns remain unaffected by postfix projections.
test649 : (x, y : Bool) -> x = y -> Bool
test649 .(x) x Refl = x
-- #441: Locals do not shadow record projections.
test441 : (Point -> Double) -> (Point -> Double) -> Point -> Double
test441 x y pt = pt.x + pt.y
-- no ambiguity errors: the locals "x" and "y" are not considered in pt.x and pt.y