individually open ≡-Reasoning
authorHelmut Grohne <helmut@subdivi.de>
Sat, 1 Aug 2020 07:05:13 +0000 (09:05 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Sat, 1 Aug 2020 07:05:13 +0000 (09:05 +0200)
commit85865ec3c7c3e3a458dc233d4c28e4db97191f3d
tree0a14606aecf7bc228f0ddd9d9af78bf37650188f
parent6ce567bf63a61bce4ccf71e3ec402d94d1da2fb1
individually open ≡-Reasoning

_≡⟨_⟩_ will be turned into a syntax, so it cannot be imported in future.
Avoid doing so now by opening it where needed.
FinMap.agda
Precond.agda