And just so I don't give the wrong impression I should not fail to
point out that this sort of dependent type does also work in SPAD:
(1) -> )sys cat dep1.spad
)abbrev domain F f
f(x:Ring) : LinearAggregate(x) == List (x)
(1) -> )co dep1.spad
Compiling FriCAS source code from file /home/page/dep1.spad using
old system compiler.
F abbreviates domain f
------------------------------------------------------------------------
initializing NRLIB F for f
compiling into NRLIB F
****** Domain: $ already in scope
augmenting $: (finiteAggregate)
****** Domain: x already in scope
augmenting x: (Evalable x)
****** Domain: $ already in scope
augmenting $: (finiteAggregate)
****** Domain: $ already in scope
augmenting $: (shallowlyMutable)
****** Domain: x already in scope
augmenting x: (ConvertibleTo (InputForm))
(time taken in buildFunctor: 0)
;;; *** |f| REDEFINED
;;; *** |f| REDEFINED
Time: 0.11 SEC.
Cumulative Statistics for Constructor f
Time: 0.11 seconds
--------------non extending category----------------------
.. f(#1) of cat
(|LinearAggregate| |#1|) has no
(|ListAggregate| |#1|) finalizing NRLIB F
Processing f for Browser database:
--->dep1.as-->f(): Missing Description
; compiling file "/home/page/F.NRLIB/F.lsp" (written 19 AUG 2011 03:14:53 PM):
; file: /home/page/F.NRLIB/F.lsp
; in: DEFUN |f;|
; (BOOT::|haddProp| BOOT::|$ConstructorCache| 'BOOT::|f| (LIST BOOT::DV$1)
; (CONS 1 BOOT::$))
;
; caught WARNING:
; undefined variable: |$ConstructorCache|
; in: DEFUN |f|
; (VMLISP:HGET BOOT::|$ConstructorCache| 'BOOT::|f|)
; --> GETHASH
; ==>
; (SB-IMPL::GETHASH3 'BOOT::|f| BOOT::|$ConstructorCache| NIL)
;
; caught WARNING:
; undefined variable: |$ConstructorCache|
;
; compilation unit finished
; Undefined variable:
; |$ConstructorCache|
; caught 2 WARNING conditions
; /home/page/F.NRLIB/F.fasl written
; compilation finished in 0:00:00.096
------------------------------------------------------------------------
f is now explicitly exposed in frame frame1
f will be automatically loaded when needed from /home/page/F.NRLIB/F
(1) -> x:f(Integer):=construct [1,2,3]
(1) [1,2,3]
Type: f(Integer)
(2) ->
On Fri, Aug 19, 2011 at 2:43 PM, Bill Page <[email protected]> wrote:
> You might be curious how this works using Aldor in FriCAS:
>
> (1) -> )sys cat dep1.as
>
> #pile
> #include "axiom.as"
> f(x:Ring) : LinearAggregate(x) == List (x)
>
> ...
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
