commit d4ad899b2effc0e1cb8adff42cc811383f2ec9cb Author: rhiannon morris Date: Wed Jul 7 13:11:39 2021 +0200 first diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..378eac2 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +build diff --git a/README.md b/README.md new file mode 100644 index 0000000..db91c2f --- /dev/null +++ b/README.md @@ -0,0 +1,6 @@ +# ![](qtuwu.png) quantitative observational extensional(ish) type theory + +hey what would happen if some idiot tried to weld qtt[^1] and xtt together? +let's find out together + +[^1]: actually grtt but wtf is a grox diff --git a/acsl.txt b/acsl.txt new file mode 100644 index 0000000..d82e332 --- /dev/null +++ b/acsl.txt @@ -0,0 +1,34 @@ +ANTI-CAPITALIST SOFTWARE LICENSE (v 1.4) + +Copyright © 2021 rhiannon morris + +This is anti-capitalist software, released for free use by individuals and +organizations that do not operate by capitalist principles. + +Permission is hereby granted, free of charge, to any person or organization +(the “User”) obtaining a copy of this software and associated documentation +files (the “Software”), to use, copy, modify, merge, distribute, and/or sell +copies of the Software, subject to the following conditions: + +1. The above copyright notice and this permission notice shall be included in + all copies or modified versions of the Software. + +2. The User is one of the following: + a. An individual person, laboring for themselves + b. A non-profit organization + c. An educational institution + d. An organization that seeks shared profit for all of its members, and + allows non-members to set the cost of their labor + +3. If the User is an organization with owners, then all owners are workers and + all workers are owners with equal equity and/or equal vote. + +4. If the User is an organization, then the User is not law enforcement or + military, or working for or under either. + +THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT EXPRESS OR IMPLIED WARRANTY OF ANY +KIND, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF +CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/qtuwu.png b/qtuwu.png new file mode 100644 index 0000000..08a92e5 Binary files /dev/null and b/qtuwu.png differ diff --git a/quox.ipkg b/quox.ipkg new file mode 100644 index 0000000..e9db42b --- /dev/null +++ b/quox.ipkg @@ -0,0 +1,12 @@ +package quox +version = 0 +license = "acsl" +authors = "rhiannon morris" +-- homepage = "..." +sourceloc = "https://git.rhiannon.website/rhi/quox" + +executable = quox +main = Quox +sourcedir = "src" + +depends = base diff --git a/src/Quox.idr b/src/Quox.idr new file mode 100644 index 0000000..39512b5 --- /dev/null +++ b/src/Quox.idr @@ -0,0 +1,4 @@ +module Quox + +main : IO Unit +main = putStrLn ":qtuwu:"