summaryrefslogtreecommitdiff
path: root/kernel/term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.ml')
-rw-r--r--kernel/term.ml23
1 files changed, 15 insertions, 8 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index c920c80b..1f3d2635 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: term.ml 10859 2008-04-27 16:46:15Z herbelin $ *)
+(* $Id: term.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
(* This module instantiates the structure of generic deBruijn terms to Coq *)
@@ -370,16 +370,22 @@ let destProd c = match kind_of_term c with
| Prod (x,t1,t2) -> (x,t1,t2)
| _ -> invalid_arg "destProd"
+let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
+
(* Destructs the abstraction [x:t1]t2 *)
let destLambda c = match kind_of_term c with
| Lambda (x,t1,t2) -> (x,t1,t2)
| _ -> invalid_arg "destLambda"
+let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
+
(* Destructs the let [x:=b:t1]t2 *)
let destLetIn c = match kind_of_term c with
| LetIn (x,b,t1,t2) -> (x,b,t1,t2)
| _ -> invalid_arg "destProd"
+let isLetIn c = match kind_of_term c with LetIn _ -> true | _ -> false
+
(* Destructs an application *)
let destApp c = match kind_of_term c with
| App (f,a) -> (f, a)
@@ -389,10 +395,6 @@ let destApplication = destApp
let isApp c = match kind_of_term c with App _ -> true | _ -> false
-let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
-
-let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
-
(* Destructs a constant *)
let destConst c = match kind_of_term c with
| Const kn -> kn
@@ -419,22 +421,27 @@ let destConstruct c = match kind_of_term c with
| Construct (kn, a as r) -> r
| _ -> invalid_arg "dest"
-let isConstruct c = match kind_of_term c with
- Construct _ -> true | _ -> false
+let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false
(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
let destCase c = match kind_of_term c with
| Case (ci,p,c,v) -> (ci,p,c,v)
| _ -> anomaly "destCase"
+let isCase c = match kind_of_term c with Case _ -> true | _ -> false
+
let destFix c = match kind_of_term c with
| Fix fix -> fix
| _ -> invalid_arg "destFix"
-
+
+let isFix c = match kind_of_term c with Fix _ -> true | _ -> false
+
let destCoFix c = match kind_of_term c with
| CoFix cofix -> cofix
| _ -> invalid_arg "destCoFix"
+let isCoFix c = match kind_of_term c with CoFix _ -> true | _ -> false
+
(******************************************************************)
(* Cast management *)
(******************************************************************)