Domain "Exit" is the bottom type in type theory:

https://en.wikipedia.org/wiki/Bottom_type


diff --git a/src/algebra/any.spad b/src/algebra/any.spad
index 4d46a77c..ada256fe 100644
--- a/src/algebra/any.spad
+++ b/src/algebra/any.spad
@@ -202,15 +202,18 @@
 ++ Examples:
 ++ References:
 ++ Description:
-++   A function which does not return directly to its caller should
+++   \spadtype{Exit} implements the bottom type in type theory.
+++   It is the type that has no value. A function which does not
+++   return directly to its caller should
 ++   have Exit as its return type.
 ++
 ++   Note: It is convenient to have a formal \spad{coerce} into each type from
 ++   type Exit. This allows, for example, errors to be raised in
 ++   one half of a type-balanced \spad{if}.
-Exit : SetCategory == add
-        coerce(n:%) == error "Cannot use an Exit value."
-        n1 = n2     == error "Cannot use an Exit value."
+Exit : Type == add
+    -- currently we can't have an empty body for "add" in pile mode
+    -- the following is just a placeholder
+    id(x : %) : % == x

 )abbrev package RESLATC ResolveLatticeCompletion
 ++ Author: Stephen M. Watt
diff --git a/src/algebra/error.spad b/src/algebra/error.spad
index b14b6969..5910fef3 100644
--- a/src/algebra/error.spad
+++ b/src/algebra/error.spad
@@ -58,10 +58,7 @@
     prefix2 : String := "Error signalled from user code in function %b "

     doit(s : String) : Exit ==
-      throwPatternMsg(s, []$(List String))$Lisp
-      -- there are no objects of type Exit, so we'll fake one,
-      -- knowing we will never get to this step anyway.
-      "exit" pretend Exit
+        throwPatternMsg(s, NIL)$Lisp pretend Exit

     error(s : String) : Exit ==
       doit concat [prefix1, s]

-- 
You received this message because you are subscribed to the Google Groups 
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.

Reply via email to