A categorical programming language
修订版 | 9d5217685979ed7890a78bc374a7a9af1ca6ea67 (tree) |
---|---|
时间 | 2023-03-28 05:46:40 |
作者 | Corbin <cds@corb...> |
Commiter | Corbin |
Add a few more rules for Booleans.
@@ -223,6 +223,7 @@ fn main() -> std::io::Result<()> { | ||
223 | 223 | // 2 = 1 + 1 |
224 | 224 | rw!("bool-t-either"; "(comp t either)" => "left"), |
225 | 225 | rw!("bool-f-either"; "(comp f either)" => "right"), |
226 | + rw!("bool-not-either"; "(comp (comp not either) (case ?f ?g))" => "(comp either (case ?g ?f))"), | |
226 | 227 | |
227 | 228 | // Boolean negation |
228 | 229 | rw!("bool-t-not"; "(comp t not)" => "f"), |
@@ -239,6 +240,10 @@ fn main() -> std::io::Result<()> { | ||
239 | 240 | rw!("bool-conj-t-pointed"; "(comp (pair (comp ignore t) ?b) conj)" => "?b"), |
240 | 241 | rw!("bool-disj-f-pointed"; "(comp (pair (comp ignore f) ?b) disj)" => "?b"), |
241 | 242 | rw!("bool-disj-t-pointed"; "(comp (pair (comp ignore t) ?b) disj)" => "(comp ignore t)"), |
243 | + rw!("bool-conj-dup"; "(comp dup conj)" => "id"), | |
244 | + rw!("bool-disj-dup"; "(comp dup disj)" => "id"), | |
245 | + rw!("bool-conj-not"; "(comp (pair not id) conj)" => "(comp ignore f)"), | |
246 | + rw!("bool-disj-not"; "(comp (pair not id) disj)" => "(comp ignore t)"), | |
242 | 247 | |
243 | 248 | // IEEE 754 addition |
244 | 249 | // f-add is symmetric |