@@ -15,14 +15,14 @@
1515 undeclared fixity are treated as non-associative with precedence lower
1616 than all declared operators.
1717+ 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}`.
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}`.
2626
2727## Library Updates
2828