Commit be766197 authored by Robbert Krebbers's avatar Robbert Krebbers

Make namespace type classes opaque.

This way we ensure that Coq gives an error message when one accidentially
writes "N ⊆ E" instead of "nclose N ⊆ E". Before, it used the ⊆ instance of
lists.
parent 2a909937
Pipeline #2658 passed with stage
in 9 minutes
......@@ -2,6 +2,10 @@ From iris.prelude Require Export countable coPset.
From iris.algebra Require Export base.
Definition namespace := list positive.
Instance namespace_dec (N1 N2 : namespace) : Decision (N1 = N2) := _.
Instance namespace_countable : Countable namespace := _.
Typeclasses Opaque namespace.
Definition nroot : namespace := nil.
Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment