Merge pull request #3711 from FStarLang/_nik_remove_admit

Nik remove admit
FStarLang · Jan 31, 2025 · 8a81ab2 · 8a81ab2
2 parents 9836dc3 + 0aad5fa
commit 8a81ab2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/ulib/FStar.FunctionalQueue.fst b/ulib/FStar.FunctionalQueue.fst
@@ -144,7 +144,7 @@ let lemma_snoc_list_seq (#a:Type) (x:a) (q:queue a)
     seq_of_list l `Seq.append` seq_of_list [x];
     == { assert (Seq.equal (seq_of_list [x]) (Seq.create 1 x)) }
     seq_of_list l `Seq.append` Seq.create 1 x;
-    == { admit() }
+    == { }
     Seq.snoc (seq_of_list l) x;
   }