Compare commits
No commits in common. "7d5b39f130d161d9bdb426e8b557ba3dc85b1b10" and "392b103f38453733dd6fc128af95cba9e00beaba" have entirely different histories.
7d5b39f130
...
392b103f38
@ -428,7 +428,6 @@ and already be up-to-speed on a big chunk of the content.
|
||||
{{< /block >}}
|
||||
|
||||
#### Rules
|
||||
{{< foldtable >}}
|
||||
| Rule | Description |
|
||||
|--------------|-------------|
|
||||
| {{< latex >}}s : \text{string} {{< /latex >}}| String literals have type \\(\\text{string}\\) |
|
||||
|
@ -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
|
||||
{{< sidenote "right" "rules-note" "previously used." >}}
|
||||
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
|
||||
rules work together below.
|
||||
{{< /sidenote >}} I will also give a quick
|
||||
summary of each of these rules.
|
||||
|
||||
{{< foldtable >}}
|
||||
Rule|Name and Description
|
||||
-----|-------
|
||||
{{< latex >}}
|
||||
|
@ -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:
|
||||
true and false. Why don't we do the same thing?
|
||||
|
||||
{{< foldtable >}}
|
||||
|UCC Spec| Coq encoding |
|
||||
|---|----|
|
||||
|\\(\\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:
|
||||
|
||||
{{< foldtable >}}
|
||||
|UCC Spec| Coq encoding |
|
||||
|---|----|
|
||||
|\\(\\text{or}\\)=\\(\\text{clone}\\ \\text{apply}\\)| {{< codelines "Coq" "dawn/Dawn.v" 65 65 >}}
|
||||
|
@ -1 +1 @@
|
||||
Subproject commit 869f9d12c84ebf38fe8f21611af9d3bf7ff5ea0d
|
||||
Subproject commit c5a28bf7ef0ea0ec4f534cf2bff231d1ad43bcea
|
Loading…
Reference in New Issue
Block a user