format

ufmg-smite · Oct 13, 2024 · fa7bcb4 · fa7bcb4
1 parent c77cb5c
commit fa7bcb4
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 14 deletions.
diff --git a/carcara/src/ast/polyeq.rs b/carcara/src/ast/polyeq.rs
@@ -10,8 +10,7 @@
 use rug::Rational;
 
 use super::{
-    AnchorArg, BindingList, Constant, Operator, ProofCommand, ProofStep, Rc, Sort,
-    Subproof, Term,
+    AnchorArg, BindingList, Constant, Operator, ProofCommand, ProofStep, Rc, Sort, Subproof, Term,
 };
 use crate::utils::HashMapStack;
 use std::time::{Duration, Instant};

diff --git a/carcara/src/checker/rules/quantifier.rs b/carcara/src/checker/rules/quantifier.rs
@@ -31,8 +31,7 @@ pub fn forall_inst(
                     QuantifierError::NoBindingMatchesArg(var_name.clone())
                 );
                 Ok((var.clone(), value.clone()))
-            }
-            else {
+            } else {
                 Err(QuantifierError::ArgNotVar(var.clone()).into())
             }
         })

diff --git a/carcara/src/elaborator/mod.rs b/carcara/src/elaborator/mod.rs
@@ -223,10 +223,7 @@ impl<'e> Elaborator<'e> {
             clause: vec![term.clone()],
             rule: "resolution".to_owned(),
             premises: vec![new_assume, equiv1_step],
-            args: vec![
-                premise,
-                self.pool.bool_true(),
-            ],
+            args: vec![premise, self.pool.bool_true()],
             ..Default::default()
         }))
     }

diff --git a/carcara/src/elaborator/resolution.rs b/carcara/src/elaborator/resolution.rs
@@ -27,9 +27,7 @@ pub fn resolution(
                     clause: Vec::new(),
                     rule: "resolution".to_owned(),
                     premises: vec![step.premises[0].clone(), true_step],
-                    args: [true, false]
-                        .map(|a| pool.bool_constant(a))
-                        .to_vec(),
+                    args: [true, false].map(|a| pool.bool_constant(a)).to_vec(),
                     ..Default::default()
                 })));
             }

diff --git a/carcara/src/parser/tests.rs b/carcara/src/parser/tests.rs
@@ -643,9 +643,12 @@ fn test_step() {
             premises: Vec::new(),
             args: {
                 vec![
-                    p.add(Term::new_var("a", int_sort.clone())), p.add(Term::new_int(12)),
-                    p.add(Term::new_var("b", real_sort)), p.add(Term::new_real((314, 100))),
-                    p.add(Term::new_var("c", int_sort)), parse_term(&mut p, "(* 6 7)"),
+                    p.add(Term::new_var("a", int_sort.clone())),
+                    p.add(Term::new_int(12)),
+                    p.add(Term::new_var("b", real_sort)),
+                    p.add(Term::new_real((314, 100))),
+                    p.add(Term::new_var("c", int_sort)),
+                    parse_term(&mut p, "(* 6 7)"),
                 ]
             },
             discharge: Vec::new(),