From d31101103fae2d2b85d83d628183b91f90912782 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Tue, 24 Sep 2024 12:08:00 +0200
Subject: [PATCH] coq: add expr_fv_type

---
 coq/terms/debruijn.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/coq/terms/debruijn.v b/coq/terms/debruijn.v
index f6e0505..9ecf6bc 100644
--- a/coq/terms/debruijn.v
+++ b/coq/terms/debruijn.v
@@ -187,6 +187,21 @@ Fixpoint expr_fv (e : expr_DeBruijn) {struct e} : atoms :=
   | ex_descend τ t' => (expr_fv t')
   end.
 
+(* get the list of all free type variables in an expression *)
+Fixpoint expr_fv_type (e : expr_DeBruijn) {struct e} : atoms :=
+  match e with
+  | ex_fvar n => {}
+  | ex_bvar y => {}
+  | ex_ty_abs t' => {}
+  | ex_ty_app t' σ => (expr_fv_type t') `union` (type_fv σ)
+  | ex_morph σ t' => (type_fv σ) `union` (expr_fv_type t')
+  | ex_abs σ t' => (type_fv σ) `union` (expr_fv_type t')
+  | ex_app t1 t2 => (expr_fv_type t1) `union` (expr_fv_type t2)
+  | ex_let t1 t2 => (expr_fv_type t1) `union` (expr_fv_type t2)
+  | ex_ascend τ t' => (expr_fv_type t')
+  | ex_descend τ t' => (expr_fv_type t')
+  end.
+
 (* substitute free variable x with expression s in t *)
 Fixpoint expr_subst (x:atom) (s:expr_DeBruijn) (t:expr_DeBruijn) {struct t} : expr_DeBruijn :=
   match t with