[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re
From: |
Gabriel Dos Reis |
Subject: |
[Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: iterators and cartesian product. |
Date: |
Mon, 22 Oct 2007 12:15:08 -0500 (CDT) |
On Mon, 22 Oct 2007, Bill Page wrote:
| Yes, that is the point. Apparently Stephen Watt's answer in Aldor is
| that allow the domain of 'Domain' to be 'Domain' is ok provided we are
| careful exactly what operations we expect to provide in 'Domain'.
Domain:Domain introduces an inconsistency at its Curry-Howard logic
level, so I'm nervous about that. A solution, adopted by Coq, is that
even though the interface would display Type:Type, what it really does
it that it has an infinite hierarchy of universes Type(k), where
Type(i) : Type(j), for i < j, starting from 0.
-- Gaby
- [Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., (continued)
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Francois Maltey, 2007/10/31
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Bill Page, 2007/10/31
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Francois Maltey, 2007/10/31
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Bill Page, 2007/10/31
- Message not available
- [Axiom-math] Fwd: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Bill Page, 2007/10/31
- Message not available
- Message not available
- [Axiom-math] Fwd: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Bill Page, 2007/10/31
- [Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: iterators and cartesian product., Gabriel Dos Reis, 2007/10/22
- [Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: iterators and cartesian product.,
Gabriel Dos Reis <=
- [Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: iterators and cartesian product., Gabriel Dos Reis, 2007/10/22
- [Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: iterators and cartesian product., Gabriel Dos Reis, 2007/10/22
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Ralf Hemmecke, 2007/10/23
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Gabriel Dos Reis, 2007/10/23
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Ralf Hemmecke, 2007/10/23
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Gabriel Dos Reis, 2007/10/23
- [Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Bill Page, 2007/10/23
- [Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Ralf Hemmecke, 2007/10/23
- [Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Bill Page, 2007/10/23
- [Axiom-math] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product., Ralf Hemmecke, 2007/10/23