summaryrefslogtreecommitdiff
path: root/src/Obs.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2022-12-08 10:33:21 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2022-12-08 10:35:16 +0000
commit4fa5948dafdb102ad0ab1cd3753d910929534673 (patch)
tree98c542ce291dc4942bc506f5be2b28b0604ba15e /src/Obs.idr
Initial commit.
Diffstat (limited to 'src/Obs.idr')
-rw-r--r--src/Obs.idr0
1 files changed, 0 insertions, 0 deletions
diff --git a/src/Obs.idr b/src/Obs.idr
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/Obs.idr