Added a readme for the formalization.

mcoblenz · Jul 2, 2020 · 04c48ee · 04c48ee
1 parent 80e03d6
commit 04c48ee
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/formalization/README.txt b/formalization/README.txt
@@ -0,0 +1,2 @@
+This directory contains a mechanization in Agda of a very small fragment of 
+Silica, consisting only of variables. I stopped working on this after determining that mechanizing the entire Silica language would take a prohibitive amount of time. Nonetheless, some key properties of Silica are proved here, so I am keeping this around as evidence of those properties.