Function compile_const

crates/compile/src/compile.rs:3004–3013

Compile a single constant.

(
  name: &Name,
  all: &NameSet,
  lean_env: &Arc<LeanEnv>,
  cache: &mut BlockCache,
  stt: &CompileState,
  kctx: &mut KernelCtx,
)

            )?,
            || {
              compare_expr(
                &x.value,
                &y.value,
                mut_ctx,
                &x.level_params,
                &y.level_params,
                stt,
              )
            },
          )
        },
      )
    },