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