From e70d2fac01253cddee14d0fe7716dc5cf61e5ec1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Thu, 7 Oct 2021 18:59:43 -0300 Subject: [PATCH] move example --- example/example.html | 4 ++++ example.lagda.md => example/example.lagda.md | 0 example/example.md | 5 +++++ 3 files changed, 9 insertions(+) create mode 100644 example/example.html rename example.lagda.md => example/example.lagda.md (100%) create mode 100644 example/example.md diff --git a/example/example.html b/example/example.html new file mode 100644 index 0000000..78e1a4c --- /dev/null +++ b/example/example.html @@ -0,0 +1,4 @@ +

This is a literate Agda file. This span - span - will be linked to the record below:

+
record span : Set where
+  constructor hey-look
+
diff --git a/example.lagda.md b/example/example.lagda.md similarity index 100% rename from example.lagda.md rename to example/example.lagda.md diff --git a/example/example.md b/example/example.md new file mode 100644 index 0000000..6e99f08 --- /dev/null +++ b/example/example.md @@ -0,0 +1,5 @@ +This is a literate Agda file. This span - `span` - will be linked to the record below: + +
record span : Set where
+  constructor hey-look
+
\ No newline at end of file