Function test_compile_expr_app

crates/compile/src/compile.rs:4029–4044

()

  // `compile_single_def` produces for a non-mutual Lean Defn.
  //
  // Inductives are never unwrapped — their projection scheme requires
  // the block.
  if ixon_mutuals.len() == 1
    && !matches!(&ixon_mutuals[0], IxonMutConst::Indc(_))
  {
    let single = ixon_mutuals.pop().unwrap();
    let result = match single {
      IxonMutConst::Defn(def) => apply_sharing_to_definition_with_stats(
        def,
        refs,
        univs,
        Some(&name_str),
      ),
      IxonMutConst::Recr(rec) => {
        apply_sharing_to_recursor_with_stats(rec, refs, univs)
      },
      IxonMutConst::Indc(_) => unreachable!(),
    };
    let standalone_constant = result.constant;