From f027346d52fa0006c5d9b348ebcc71ec401692b7 Mon Sep 17 00:00:00 2001 From: Nick Drozd Date: Thu, 11 Jun 2020 19:00:21 -0500 Subject: [PATCH] Add note about `cong` --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index d90ba9e43..ca4ceb1e8 100644 --- a/README.md +++ b/README.md @@ -34,6 +34,7 @@ exceptions. The most notable user visible differences, which might cause Idris (such as data constructors), or which have different concrete argument types (such as record projections). It may struggle to resolve ambiguities if one name requires an interface to be resolved. ++ The `cong` function now takes its congruence explicitly as its first argument. + Minor differences in the meaning of export modifiers `private`, `export`, and `public export`, which now refer to visibility of names from other *namespaces* rather than visibility from other *files*.