Add CHANGELOG entry and test
commit8da55c25058245bb8bd6387a9517c99ae8d8184f
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateWed 8 Nov 2017, 21:10 (9 years ago)
parent6318168
CHANGELOG.md+9
@@ -14,6 +14,15 @@
1414 other operators, e.g. ``infixr 8 `cons` ``. Backticked operators with
1515 undeclared fixity are treated as non-associative with precedence lower
1616 than all declared operators.
17++ Allow non-injective implementations if explicitly named, e.g.,
18+```idris
19+LTB : Nat -> Type
20+LTB b = DPair Nat (\ n => LT n b)
21+
22+implementation [uninhabltb] Uninhabited (LTB Z) where
23+ uninhabited (MkDPair n prf) = absurd prf
24+```
25+It is possible to use `using implementation uninhabltb` to add the implementation to the automated resolution, but if it fails to find the instance due to non-injectivity, one must pass it explicitly to target function, i.e. `absurd @{uninhabltb}`.
1726
1827## Library Updates
1928
test/interfaces009/expectednew file
No changes to the content.
test/interfaces009/interfaces009.idrnew file+24
@@ -0,0 +1,24 @@
1+module Test
2+
3+LTE : (x, y : Double) -> Type
4+
5+NonNegDouble : Type
6+NonNegDouble = Subset Double (\ x => 0.0 `LTE` x)
7+
8+plus : (x, y : NonNegDouble) -> NonNegDouble
9+
10+mult : (x, y : NonNegDouble) -> NonNegDouble
11+
12+fromIntegerNN : Integer -> NonNegDouble
13+
14+implementation [numnnd] Num NonNegDouble where
15+ (+) = plus
16+ (*) = mult
17+ fromInteger = fromIntegerNN
18+
19+using implementation numnnd
20+ x : NonNegDouble
21+ y : NonNegDouble
22+ z : NonNegDouble
23+ z = x + y
24+
test/interfaces009/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces009.idr --noprelude --check
3+rm -f interfaces009 *.ibc