Added nonempty_sort.
authornipkow
Tue Aug 01 12:36:05 1995 +0200 (1995-08-01)
changeset 12143f3888213ceb
parent 1213 a8f6d0fa2a59
child 1215 a206f722bef9
Added nonempty_sort.
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Fri Jul 28 19:17:03 1995 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Aug 01 12:36:05 1995 +0200
     1.3 @@ -62,6 +62,7 @@
     1.4      val add_name: string -> sg -> sg
     1.5      val make_draft: sg -> sg
     1.6      val merge: sg * sg -> sg
     1.7 +    val nonempty_sort: sg * sort list * sort -> bool
     1.8      val proto_pure: sg
     1.9      val pure: sg
    1.10      val cpure: sg
    1.11 @@ -551,4 +552,11 @@
    1.12    |> add_syntax Syntax.pure_applC_syntax
    1.13    |> add_name "CPure";
    1.14  
    1.15 +(**
    1.16 +Emptiness-test for sorts: does there exist a type of sort 'sort' whose
    1.17 +vars have sorts contained in 'sorts'?
    1.18 +Trivial approximation at the moment.
    1.19 +**)
    1.20 +fun nonempty_sort(_,sorts,sort) = exists (fn s => sort subset s) sorts;
    1.21 +
    1.22  end;