@@ -15,14 +15,14 @@
15 undeclared fixity are treated as non-associative with precedence lower
15 undeclared fixity are treated as non-associative with precedence lower
16 than all declared operators.
16 than all declared operators.
17+ Allow non-injective implementations if explicitly named, e.g.,
17+ Allow non-injective implementations if explicitly named, e.g.,
19−LTB : Nat -> Type
19+ LTB : Nat -> Type
20−LTB b = DPair Nat (\ n => LT n b)
20+ LTB b = DPair Nat (\ n => LT n b)
22−implementation [uninhabltb] Uninhabited (LTB Z) where
22+ implementation [uninhabltb] Uninhabited (LTB Z) where
23− uninhabited (MkDPair n prf) = absurd prf
23+ uninhabited (MkDPair n prf) = absurd prf
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}`.
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}`.
27## Library Updates
27## Library Updates