From df663290f60a576a767164024219531ac225530e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2023 11:51:40 +0200
Subject: [PATCH] Test case for `TCSimpl`.

---
 tests/typeclasses.ref |  8 ++++++++
 tests/typeclasses.v   | 14 +++++++++++++-
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/tests/typeclasses.ref b/tests/typeclasses.ref
index e69de29b..55c62f13 100644
--- a/tests/typeclasses.ref
+++ b/tests/typeclasses.ref
@@ -0,0 +1,8 @@
+"tc_simpl_test"
+     : string
+1 goal
+  
+  P : nat → Prop
+  y : nat
+  ============================
+  P (S (S (S (S (S (S y))))))
diff --git a/tests/typeclasses.v b/tests/typeclasses.v
index 899518d5..500bf046 100644
--- a/tests/typeclasses.v
+++ b/tests/typeclasses.v
@@ -1,4 +1,16 @@
-From stdpp Require Import prelude.
+From stdpp Require Import strings.
+
+Lemma tc_simpl_test_lemma (P : nat → Prop) x y :
+  TCSimpl x y →
+  P x → P y.
+Proof. by intros ->%TCSimpl_eq. Qed.
+
+Check "tc_simpl_test".
+Lemma tc_simpl_test (P : nat → Prop) y : P (5 + S y).
+Proof.
+  apply (tc_simpl_test_lemma _ _ _ _). (* would be nicer with ssr [apply:] *)
+  Show.
+Abort.
 
 (** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
     Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
-- 
GitLab