From 191bfcddc19676b141274c4675002565255be537 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 24 Feb 2020 19:32:57 -0800 Subject: [PATCH] chore: remove `#exit` --- src/Init/MaxSharing.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Init/MaxSharing.lean b/src/Init/MaxSharing.lean index fe085ce11c..33b8fec47c 100644 --- a/src/Init/MaxSharing.lean +++ b/src/Init/MaxSharing.lean @@ -88,8 +88,6 @@ unsafe def ObjectPersistentSet.find? (s : ObjectPersistentSet) (o : Object) : Op unsafe def ObjectPersistentSet.insert (s : ObjectPersistentSet) (o : Object) : ObjectPersistentSet := @PersistentHashSet.insert Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o -#exit -- REMOVE after update stage0 - /- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet` -/ constant StatePointed : PointedType := arbitrary _ abbrev State : Type := StatePointed.type