Gabriel Dos Reis <[EMAIL PROTECTED]> writes: > | > | if R has FiniteFieldCategory and (-1 is not a square in R) then Field > | > | The condition (-1 is not a square in R) could be computed using something > like > | > | > ------------------------------------------------------------------------------- > | Help(F: FiniteFieldCategory): C == T where > | C == with > | help: () -> Boolean > | > | T == add > | help() == one?(size()$F rem 4) > | > ------------------------------------------------------------------------------- > | > | so we'd then have > | > | if R has FiniteFieldCategory and help()$Help(R) then Field > | > | > | Do you think that's doable? > > One has to find ways to compile that without having to evaluate > runtime entities (juste like we currently do with `has' expressions).
I'd be extremely surprised if that were possible. I'm quite sure it isn't. I.e., it is necessary to extend the compiler allow runtime evaluation within conditional exports. Otherwise, we have a quite severe restriction on what can be done with SPAD. I guess, as severe as or even more severe than not having dependent types in arbitrary functions. > ... but in the immediate future this is not something I'm working on -- I > have pressing regressions to fix first. Too bad. I was hoping I could get you hooked. Merry Christmas, Martin ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2005. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
