From 42cdeefac13c8cd61bac5ecc14a3f1cdc9f90983 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 14:16:29 +0200
Subject: [PATCH] add binder_list

---
 theories/binders.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/binders.v b/theories/binders.v
index 1bdd40a0..36f9893e 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -19,6 +19,13 @@ Inductive binder := BAnon | BNamed :> string → binder.
 Bind Scope binder_scope with binder.
 Notation "<>" := BAnon : binder_scope.
 
+(** [binder_list] matches [option_list]. *)
+Definition binder_list (b : binder) : list string :=
+  match b with
+  | BAnon => []
+  | BNamed s => [s]
+  end.
+
 Global Instance binder_dec_eq : EqDecision binder.
 Proof. solve_decision. Defined.
 Global Instance binder_inhabited : Inhabited binder := populate BAnon.
-- 
GitLab