Compare commits

..

No commits in common. "7d5b39f130d161d9bdb426e8b557ba3dc85b1b10" and "392b103f38453733dd6fc128af95cba9e00beaba" have entirely different histories.

4 changed files with 2 additions and 6 deletions

View File

@ -428,7 +428,6 @@ and already be up-to-speed on a big chunk of the content.
{{< /block >}} {{< /block >}}
#### Rules #### Rules
{{< foldtable >}}
| Rule | Description | | Rule | Description |
|--------------|-------------| |--------------|-------------|
| {{< latex >}}s : \text{string} {{< /latex >}}| String literals have type \\(\\text{string}\\) | | {{< latex >}}s : \text{string} {{< /latex >}}| String literals have type \\(\\text{string}\\) |

View File

@ -58,13 +58,12 @@ __generalization__ and __instantiation__. It's been quite a while since the last
to present a table with these new rules, as well as all of the ones that we to present a table with these new rules, as well as all of the ones that we
{{< sidenote "right" "rules-note" "previously used." >}} {{< sidenote "right" "rules-note" "previously used." >}}
The rules aren't quite the same as the ones we used earlier; The rules aren't quite the same as the ones we used earlier;
note that \(\sigma\) is used in place of \(\tau\) in the first rule, note that \\(\sigma\\) is used in place of \\(\tau\\) in the first rule,
for instance. These changes are slight, and we'll talk about how the for instance. These changes are slight, and we'll talk about how the
rules work together below. rules work together below.
{{< /sidenote >}} I will also give a quick {{< /sidenote >}} I will also give a quick
summary of each of these rules. summary of each of these rules.
{{< foldtable >}}
Rule|Name and Description Rule|Name and Description
-----|------- -----|-------
{{< latex >}} {{< latex >}}

View File

@ -219,7 +219,6 @@ Here, we may as well go through the three constructors to explain what they mean
Now it's time for some fun! The UCC language specification starts by defining two values: Now it's time for some fun! The UCC language specification starts by defining two values:
true and false. Why don't we do the same thing? true and false. Why don't we do the same thing?
{{< foldtable >}}
|UCC Spec| Coq encoding | |UCC Spec| Coq encoding |
|---|----| |---|----|
|\\(\\text{false}\\)=\\([\\text{drop}]\\)| {{< codelines "Coq" "dawn/Dawn.v" 41 42 >}} |\\(\\text{false}\\)=\\([\\text{drop}]\\)| {{< codelines "Coq" "dawn/Dawn.v" 41 42 >}}
@ -258,7 +257,6 @@ element, as specified. The proof for \\(\\text{true}\\) is very similar in spiri
We can also formalize the \\(\\text{or}\\) operator: We can also formalize the \\(\\text{or}\\) operator:
{{< foldtable >}}
|UCC Spec| Coq encoding | |UCC Spec| Coq encoding |
|---|----| |---|----|
|\\(\\text{or}\\)=\\(\\text{clone}\\ \\text{apply}\\)| {{< codelines "Coq" "dawn/Dawn.v" 65 65 >}} |\\(\\text{or}\\)=\\(\\text{clone}\\ \\text{apply}\\)| {{< codelines "Coq" "dawn/Dawn.v" 65 65 >}}

@ -1 +1 @@
Subproject commit 869f9d12c84ebf38fe8f21611af9d3bf7ff5ea0d Subproject commit c5a28bf7ef0ea0ec4f534cf2bff231d1ad43bcea