[limits] Add example from #484

ejgallego · May 10, 2024 · f2c31e9 · f2c31e9
1 parent 59a859a
commit f2c31e9
Showing 1 changed file with 20 additions and 0 deletions.
diff --git a/examples/int_tc_loop.v b/examples/int_tc_loop.v
@@ -0,0 +1,20 @@
+(* From https://github.com/ejgallego/coq-lsp/issues/484, thanks ! *)
+From Coq Require Import Prelude.
+
+Axiom Loop : Type.
+Existing Class Loop.
+
+Axiom loop : Loop -> Loop.
+#[export] Existing Instance loop.
+
+Global Instance foo : Loop.
+Proof. Admitted.
+
+Goal Loop.
+exact _.
+
+(* Some extra content as to test goals here *)
+Lemma foo : True.
+Proof.
+
+Qed.