This commit is contained in:
Michael Zhang 2022-10-13 01:53:13 -05:00
parent 42d3b9452b
commit a18f581ff0
11 changed files with 95 additions and 1 deletions

1
.gitignore vendored Normal file
View file

@ -0,0 +1 @@
*.agdai

View file

@ -0,0 +1,2 @@
include: src
depend: standard-library

View file

@ -1,5 +1,5 @@
```
{#- OPTIONS --cubical -#}
{-# OPTIONS --cubical #-}
----------

View file

@ -0,0 +1,8 @@
2022 Oct 10
===
```agda
{-# OPTIONS --cubical #-}
-- Hello
```

8
src/Dedekind/Bool.agda Normal file
View file

@ -0,0 +1,8 @@
module Dedekind.Bool where
-- Booleans
data Bool : Set where
true : Bool
false : Bool

View file

@ -0,0 +1,8 @@
module Dedekind.Integer where
open import Dedekind.Natural using ()
-- Integers
data : Set where
pos :
negsuc :

15
src/Dedekind/Natural.agda Normal file
View file

@ -0,0 +1,15 @@
module Dedekind.Natural where
open import Dedekind.Set using (; )
-- Natural
data : Set where
zero :
suc :
NonZero : Set
NonZero zero =
NonZero (suc n) =
gcd : (x y : ) .{{ _ : NonZero x }} .{{ _ : NonZero y }}
gcd x y = ?

View file

@ -0,0 +1,12 @@
module Dedekind.Rational where
open import Dedekind.Bool using (Bool)
open import Dedekind.Integer using ()
open import Dedekind.Natural using (; NonZero)
-- Rational
data : Set where
rat : (d : ) .{{ _ : NonZero d }}
_<_ : Bool
x < y = ?

20
src/Dedekind/Real.agda Normal file
View file

@ -0,0 +1,20 @@
-- Dedekind cuts using Cubical Agda
{-# OPTIONS --cubical #-}
module Dedekind.Real where
open import Dedekind.Rational using (; _<_)
-- Dedekind cuts
record : Set where
constructor real
field
lower : ( Bool)
closed : (x y : ) x < y
-- Operations on reals
_+_ :
a + b = real
(λ q .lower a q)
-- Properties of reals

6
src/Dedekind/Set.agda Normal file
View file

@ -0,0 +1,6 @@
module Dedekind.Set where
record : Set where
record : Set where
instance constructor tt

14
src/main.agda Normal file
View file

@ -0,0 +1,14 @@
{-# OPTIONS --guardedness #-}
module main where
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using ()
open import Agda.Builtin.String using (String)
postulate putStrLn : String IO
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}
main : IO
main = putStrLn "Hello world!"