blob: e0b86dbf27452cd1fb89d5cadafbc4c8a60326f0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* $Id$ *)
open Util
open Names
open Generic
open Term
type abstraction_body = {
abs_kind : path_kind;
abs_arity : int array;
abs_rhs : constr }
let contract_abstraction ab args =
if array_for_all2 (fun c i -> (count_dlam c) = i) args ab.abs_arity then
Sosub.soexecute (Array.fold_left sAPP ab.abs_rhs args)
else
failwith "contract_abstraction"
|
