Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ni'o jmina le ctaipe be la'o zoi. Arris ℚ ℚ .zoi. #17

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

ni'o jmina le ctaipe be la'o zoi. Arris ℚ ℚ .zoi. #17

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
f7853d9
ni'o jmina le ctaipe be la'o zoi. Arris ℚ ℚ .zoi.
varikvalefor Feb 19, 2023
db4be24
ni'o vimcu le na se pilno
varikvalefor Feb 20, 2023
52c0c4b
Merge branch 'master' into kwik-e-mart
varikvalefor Mar 19, 2023
694fcc5
Merge branch 'master' into kwik-e-mart
varikvalefor Apr 15, 2023
3c28588
Merge branch 'master' into kwik-e-mart
varikvalefor Sep 26, 2023
d49494b
Merge branch 'master' into kwik-e-mart
varikvalefor Nov 19, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 40 additions & 0 deletions src/Truthbrary/Record/Arithmetic.lagda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,13 @@ open import Data.Bool
if_then_else_
)
open import Data.Maybe
open import Data.Rational
using (
1ℚ;
0ℚ;
mkℚ;
ℚ
)
open import Data.Rational.Unnormalised as ℚᵘ
using (
1ℚᵘ;
Expand Down Expand Up @@ -246,6 +253,39 @@ instance
uyn = Data.Float.fromℕ 1
zir = Data.Float.fromℕ 0
r = const $ const Float
ariℚℚ : Arris ℚ ℚ
ariℚℚ = record {
_⊔+_ = r;
_⊔-_ = r;
_⊔*_ = r;
_⊔/_ = const $ const $ Maybe ℚ;
_+_ = Data.Rational._+_;
_-_ = Data.Rational._-_;
_*_ = Data.Rational._*_;
_/_ = deev;
uyn₁ = uyn;
uyn₂ = uyn;
uyn* = uyn;
uyn/ = just uyn;
zir₁ = zir;
zir₂ = zir;
zir+ = zir;
zir- = zir;
1*1≡1 = refl;
1/1≡1 = refl;
0+0≡0 = refl;
0-0≡0 = refl}
where
r = const $ const ℚ
uyn = 1ℚ
zir = 0ℚ
deev : ℚ → ℚ → Maybe ℚ
deev m n = spit (λ a → Data.Rational._÷_ m n {a}) $ ∣↥n∣ ≟ₙ 0
where
∣↥n∣ = Data.Integer.∣ Data.Rational.↥ n ∣
spit : (False $ ∣↥n∣ ≟ₙ 0 → ℚ) → Dec $ ∣↥n∣ ≡ 0 → Maybe ℚ
spit f (no q) = just $ f $ fromWitnessFalse q
spit _ (yes _) = nothing
ariℚᵘℚᵘ : Arris ℚᵘ ℚᵘ
ariℚᵘℚᵘ = record {
_⊔+_ = r;
Expand Down