| 4322 | let opaque = AE::cnst(mk_id("opaque"), Box::new([])); |
| 4323 | // Opaque should NOT be unfolded |
| 4324 | let result = tc.whnf(&opaque).unwrap(); |
| 4325 | assert!(matches!(result.data(), ExprData::Const(..))); |
| 4326 | } |
| 4327 | |
| 4328 | #[test] |
| 4329 | fn whnf_delta_opaque_hint_unfolds() { |
| 4330 | let mut env = env_with_id(); |
| 4331 | let mut tc = TypeChecker::new(&mut env); |
| 4332 | let opaque_def = AE::cnst(mk_id("opaque_def"), Box::new([])); |
| 4333 | let result = tc.whnf(&opaque_def).unwrap(); |
| 4334 | assert_eq!(result, sort1()); |
| 4335 | } |
| 4336 | |
| 4337 | #[test] |
| 4338 | fn major_scan_does_not_capture_an_unrelated_caller_let() { |
| 4339 | let target_id = mk_id("major-scan-target"); |
| 4340 | let mut env = KEnv::new(); |