From 49d73623b0a5d4cf0387631bad7b010f97e9cb93 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 Jul 2022 13:06:47 -0400
Subject: [PATCH] add example of using type_fixpoint
---
_CoqProject | 1 +
theories/typing/examples/fixpoint.v | 20 ++++++++++++++++++++
2 files changed, 21 insertions(+)
create mode 100644 theories/typing/examples/fixpoint.v
diff --git a/_CoqProject b/_CoqProject
index 2580fe31..388e1c67 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -85,6 +85,7 @@ theories/typing/lib/rwlock/rwlockwriteguard.v
theories/typing/lib/rwlock/rwlock_code.v
theories/typing/lib/rwlock/rwlockreadguard_code.v
theories/typing/lib/rwlock/rwlockwriteguard_code.v
+theories/typing/examples/fixpoint.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
diff --git a/theories/typing/examples/fixpoint.v b/theories/typing/examples/fixpoint.v
new file mode 100644
index 00000000..17b674c4
--- /dev/null
+++ b/theories/typing/examples/fixpoint.v
@@ -0,0 +1,20 @@
+From iris.proofmode Require Import proofmode.
+From lrust.typing Require Import typing.
+From iris.prelude Require Import options.
+
+Section fixpoint.
+ Context `{!typeGS Σ}.
+
+ Local Definition my_list_pre l : type := sum [ unit; box l].
+
+ Local Instance my_list_contractive : TypeContractive my_list_pre.
+ Proof.
+ (* FIXME: solve_type_proper should handle this. *)
+ intros n l1 l2 Hl. rewrite /my_list_pre.
+ f_equiv. constructor; last constructor; last by constructor.
+ - done.
+ - f_equiv. done.
+ Qed.
+
+ Definition my_list := type_fixpoint my_list_pre.
+End fixpoint.
--
GitLab