From b5b4cdd6a88fe88837dc6c1ecb12353f4e4c582a Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 29 Oct 2020 13:27:34 -0700
Subject: [PATCH] [sledge] Add Term.get_trm

Reviewed By: da319

Differential Revision: D24532342

fbshipit-source-id: 4c257ff41
---
 sledge/src/fol.ml  | 2 ++
 sledge/src/fol.mli | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 1b5bfc744..d245170e8 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -275,6 +275,8 @@ module Term = struct
     | `Trm (Q q) -> Some q
     | _ -> None
 
+  let get_trm = function `Trm t -> Some t | _ -> None
+
   (** Access *)
 
   let split_const e =
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index c5f910f7c..236929620 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -58,6 +58,8 @@ module rec Term : sig
   val get_const : t -> Q.t option
   (** [get_const a] is [Some q] iff [equal a (const q)] *)
 
+  val get_trm : t -> Trm.t option
+
   (** Access *)
 
   val split_const : t -> t * Q.t