From 3bcaf5d1c40b513f8e4590f7d38d3eef8393092e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 16 Jul 2020 16:46:09 +0200
Subject: Checkpoint. THIS BUILD WILL FAIL

---
 spartan/core/lib.ML | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'spartan/core/lib.ML')

diff --git a/spartan/core/lib.ML b/spartan/core/lib.ML
index 615f601..7b93a08 100644
--- a/spartan/core/lib.ML
+++ b/spartan/core/lib.ML
@@ -7,6 +7,7 @@ val maxint: int list -> int
 
 (*Terms*)
 val is_rigid: term -> bool
+val no_vars: term -> bool
 val dest_eq: term -> term * term
 val mk_Var: string -> int -> typ -> term
 val lambda_var: term -> term -> term
@@ -50,6 +51,8 @@ val maxint = max (op >)
 
 val is_rigid = not o is_Var o head_of
 
+val no_vars = not o exists_subterm is_Var
+
 fun dest_eq (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ def) = (t, def)
   | dest_eq _ = error "dest_eq"
 
-- 
cgit v1.2.3