d6
/
modal
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

add pow and rat for dealing with Q

This commit is contained in:
~d6 2024-04-14 17:01:43 -04:00
parent effc98d589
commit cfb4a8fca0
1 changed files with 13 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
arith.modal
View File

@ -331,7 +331,7 @@
<> ((pow (Z (- ?x)) (N (0 ?k)))) ((nat>pos (pow (N ?x) (N (0 ?k)))))
<> ((pow (Z (- ?x)) (N (1 ?k)))) ((nat>neg (pow (N ?x) (N (1 ?k)))))
-- ( to natural number )
-- ( to integer )
<> ((int ?*)) ((int1 (?*)))
<> ((int1 (- ?t))) ((int2 - (nat1 ?t)))
<> ((int1 (?h ?t))) ((int2 + (nat1 (?h ?t))))
@ -375,4 +375,15 @@
<> ((div (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((mul (Q (?s ?x ?d)) (Q (?t ?e ?y))))
(str (mul (Q (+ sixteen ten)) (Q (- sixteen ten))))
<> ((pow (Q (?s ?x ?d)) (N ?k))) ((qpow (pow (Z (?s ?x)) (N ?k)) (pow (N ?d) (N ?k))))
<> ((qpow (Z (?s ?n)) (N ?d))) ((ratify ?s (N ?n) (N ?d)))
-- ( to rational number )
<> ((rat ?*)) ((rat1 (?*)))
<> ((rat1 (- ?t))) ((rat2 - ?t ()))
<> ((rat1 (?h ?t))) ((rat2 + (?h ?t) ()))
<> ((rat2 ?s (/ ?t) ?a)) ((rat3 ?s (nat1 reverse ?a) (nat1 ?t)))
<> ((rat2 ?s (?h ?t) ?a)) ((rat2 ?s ?t (?h ?a)))
<> ((rat3 ?s (N ?n) (N ?d))) ((Q (?s ?n ?d)))
(str (pow (rat -2/7) (nat 3)))