Judgment fmt at crates/formality-core/src/judgment.rs:24

Signature:

fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let mut f = fmt.debug_struct(stringify!($name)); let __JudgmentStruct($($input_name),*) = self; $( f.field(stringify!($debug_input_name), $debug_input_name); )* f.finish() } } $(let $input_name: $input_ty = $crate::Upcast::upcast($input_name);)* // Assertions are preconditions. We shadow each input as a reference // so the assert expression borrows rather than consuming the variables. // // NB: we can't use `$crate` in this expression because of the `respan!` call, // which messes up `$crate` resolution. But we need the respan call for track_caller to properly // assign the span of the panic to the assertion expression and not the invocation of the judgment_fn // macro. Annoying! But our proc macros already reference `formality_core` so that seems ok. { $( #[allow(unused_variables)] let $input_name = &$input_name; )* $( $crate::respan!( $assert_expr ( formality_core::judgment::JudgmentAssertion::assert($assert_expr, stringify!($assert_expr)); ) ); )* } $( // Trivial cases are an (important) optimization that lets // you cut out all the normal rules. if $trivial_expr { let trivial_result = $trivial_result; let (file, line, column) = $crate::respan!( $trivial_expr ((file!(), line!(), column!())) ); let proof_tree = $crate::judgment::ProofTree::with_all( format!("trivial, as {} is true: {trivial_result:?}", stringify!($trivial_expr)), Default::default(), None, file, line, column, Default::default(), ); return $crate::ProvenSet::singleton((trivial_result, proof_tree)); } )* let mut failed_rules = $crate::set![]; let input = __JudgmentStruct($($input_name),*); let output = $crate::fixed_point::fixed_point::< __JudgmentStruct, $crate::Map<$output, $crate::judgment::ProofTree>, >( // Tracing span: |input| { let __JudgmentStruct($($input_name),*) = input; tracing::debug_span!( stringify!($name), $(?$debug_input_name),* ) }, // Stack: { thread_local! { static R: $crate::judgment::JudgmentStack<__JudgmentStruct, $output> = Default::default() } &R }, // Input: input.clone(), // Default value: |_| Default::default(), // Next value: |input: __JudgmentStruct| { let mut output: $crate::Map<$output, $crate::judgment::ProofTree> = $crate::Map::new(); failed_rules.clear(); #[allow(unused)] let input_string = format!("{:?}", input); $crate::push_rules!( $name, &input, output, failed_rules, &input_string, ($($input_name),*) => $output,
                        $(($($rule)*))*
                    );

                    output
                },
            );

            if !output.is_empty()

No rules discovered.