From 48833cc63b2750a8bb0cd481187d2016357cce01 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 9 Jul 2020 07:45:03 -0700
Subject: [PATCH] [sledge] Refactor: Expose constructors for record Terms

Summary: McCarthy-style select/update terms for records.

Reviewed By: jvillard

Differential Revision: D22401038

fbshipit-source-id: 9c9b8e0a1
---
 sledge/src/fol.mli | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 227a0fbe7..30a149f9b 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -88,6 +88,10 @@ module rec Term : sig
   val extract : seq:t -> off:t -> len:t -> t
   val concat : t array -> t
 
+  (* records *)
+  val select : rcd:t -> idx:int -> t
+  val update : rcd:t -> idx:int -> elt:t -> t
+
   (* if-then-else *)
   val ite : cnd:Formula.t -> thn:t -> els:t -> t