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 [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
