login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for SandBoxTryOutSPAD revision 2 of 2

1 2
Editor: hemmecke
Time: 2014/02/14 12:52:38 GMT+0
Note:

changed:
-)abbrev category MYMON rhxMonoid
-rhxMonoid: Category == with
)abbrev category MYMON MyMonoid
MyMonoid: Category == with

changed:
-)abbrev domain MYFUN rhxFun
-rhxFun(S: SetCategory): rhxMonoid with
-    myfun:  (S -> S) -> %
)abbrev domain MYFUN MyFun
MyFun(S: SetCategory): MyMonoid with
    coerce:  (S -> S) -> %

changed:
-    myfun(f: S -> S): % == per f
    coerce(f: S -> S): % == per f

added:
MI ==> MyFun I

changed:
-minc: rhxFun(I) := myfun inc
-mdouble: rhxFun(I) := myfun double
minc := inc :: MI
mdouble := double :: MI

Everyone is allowed to try out SPAD by editing this page. Don't be affraid to destroy anything. The purpose of this page is exactly to give a place for everyone to experiment.

Just hit the "edit" link in the upper right corner.

fricas
(1) -> <spad>
fricas
)abbrev category MYMON MyMonoid
MyMonoid: Category == with
    1: %
    _*: (%, %) -> %
rep x ==> (x@%) pretend Rep per x ==> (x@Rep) pretend %
fricas
)abbrev domain MYFUN MyFun
MyFun(S: SetCategory): MyMonoid with
    coerce:  (S -> S) -> %
    coerce: % -> (S -> S)
 == add
    Rep ==> S -> S
    coerce(f: S -> S): % == per f
    coerce(x: %): S -> S == rep x
    1: % == per((s: S): S +-> s)
    ((x: %) * (y: %)): % == per( (s: S): S +-> (rep x)(rep y)s )</spad>
fricas
Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5443222399567089399-25px001.spad
      using old system compiler.
   MYMON abbreviates category MyMonoid 
------------------------------------------------------------------------
   initializing NRLIB MYMON for MyMonoid 
   compiling into NRLIB MYMON 
;;; *** |MyMonoid| REDEFINED Time: 0 SEC.
finalizing NRLIB MYMON Processing MyMonoid for Browser database: --->-->MyMonoid(constructor): Not documented!!!! --->-->MyMonoid(((One) (%) constant)): Not documented!!!! --->-->MyMonoid((* (% % %))): Not documented!!!! --->-->MyMonoid(): Missing Description ; compiling file "/var/aw/var/LatexWiki/MYMON.NRLIB/MYMON.lsp" (written 21 FEB 2023 12:45:30 PM):
; /var/aw/var/LatexWiki/MYMON.NRLIB/MYMON.fasl written ; compilation finished in 0:00:00.007 ------------------------------------------------------------------------ MyMonoid is now explicitly exposed in frame initial MyMonoid will be automatically loaded when needed from /var/aw/var/LatexWiki/MYMON.NRLIB/MYMON
MYFUN abbreviates domain MyFun ------------------------------------------------------------------------ initializing NRLIB MYFUN for MyFun compiling into NRLIB MYFUN processing macro definition Rep ==> S -> S compiling exported coerce : S -> S -> $ MYFUN;coerce;M$;1 is replaced by f Time: 0.01 SEC.
compiling exported coerce : $ -> S -> S MYFUN;coerce;$M;2 is replaced by x Time: 0 SEC.
compiling exported One : () -> $ Time: 0 SEC.
compiling exported * : ($,$) -> $ Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |MyFun| REDEFINED
;;; *** |MyFun| REDEFINED Time: 0 SEC.
Warnings: [1] coerce: elt has no value [2] *: elt has no value
Cumulative Statistics for Constructor MyFun Time: 0.01 seconds
finalizing NRLIB MYFUN Processing MyFun for Browser database: --->-->MyFun(constructor): Not documented!!!! --->-->MyFun((coerce (% (Mapping S S)))): Not documented!!!! --->-->MyFun((coerce ((Mapping S S) %))): Not documented!!!! --->-->MyFun(): Missing Description ; compiling file "/var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN.lsp" (written 21 FEB 2023 12:45:30 PM):
; /var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN.fasl written ; compilation finished in 0:00:00.025 ------------------------------------------------------------------------ MyFun is now explicitly exposed in frame initial MyFun will be automatically loaded when needed from /var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN

fricas
I ==> Integer
Type: Void
fricas
II ==> I -> I
Type: Void
fricas
MI ==> MyFun I
Type: Void
fricas
inc(i: I): I == i+1
Function declaration inc : Integer -> Integer has been added to workspace.
Type: Void
fricas
double(i: I): I == 2*i
Function declaration double : Integer -> Integer has been added to workspace.
Type: Void
fricas
minc := inc :: MI
fricas
Compiling function inc with type Integer -> Integer 
LISP output: (#<FUNCTION |*1;inc;1;initial|>)
Type: MyFun?(Integer)
fricas
mdouble := double :: MI
fricas
Compiling function double with type Integer -> Integer 
LISP output: (#<FUNCTION |*1;double;1;initial|>)
Type: MyFun?(Integer)
fricas
f := (mdouble * minc) :: II

\label{eq1}\mbox{theMap (...)}(1)
Type: (Integer -> Integer)
fricas
g := (minc * mdouble) :: II

\label{eq2}\mbox{theMap (...)}(2)
Type: (Integer -> Integer)
fricas
f 1

\label{eq3}4(3)
Type: PositiveInteger?
fricas
g 1

\label{eq4}3(4)
Type: PositiveInteger?