Make most tables not wrap on small screens
This commit is contained in:
parent
dd8c846b3e
commit
7d5b39f130
@ -428,6 +428,7 @@ 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}\\) |
|
||||||
|
@ -64,6 +64,7 @@ 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 >}}
|
||||||
|
@ -219,6 +219,7 @@ 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 >}}
|
||||||
@ -257,6 +258,7 @@ 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 c5a28bf7ef0ea0ec4f534cf2bff231d1ad43bcea
|
Subproject commit 869f9d12c84ebf38fe8f21611af9d3bf7ff5ea0d
|
Loading…
Reference in New Issue
Block a user