Structural congruence after lazy delta exhaustion (lean4lean isDefEqConst/Proj). Checks Const-Const, Var-Var, Prj-Prj without further reduction.
(
&mut self,
a: &KExpr<M>,
b: &KExpr<M>,
)
| 1346 | } |
| 1347 | |
| 1348 | /// App spine comparison (lean4lean isDefEqApp): decompose both sides into |
| 1349 | /// head + args and compare componentwise. Handles multi-arg apps. |
| 1350 | fn try_def_eq_app( |
| 1351 | &mut self, |
| 1352 | a: &KExpr<M>, |
| 1353 | b: &KExpr<M>, |
| 1354 | ) -> Result<bool, TcError<M>> { |
| 1355 | if !matches!(a.data(), ExprData::App(..)) |
| 1356 | || !matches!(b.data(), ExprData::App(..)) |
| 1357 | { |
| 1358 | return Ok(false); |
| 1359 | } |
| 1360 | let (a_head, a_args) = collect_app_spine(a); |
| 1361 | let (b_head, b_args) = collect_app_spine(b); |
| 1362 | if a_args.len() != b_args.len() { |
| 1363 | return Ok(false); |
| 1364 | } |
| 1365 | if !self.is_def_eq(&a_head, &b_head)? { |
| 1366 | return Ok(false); |
| 1367 | } |
| 1368 | for (ai, bi) in a_args.iter().zip(b_args.iter()) { |
| 1369 | if !self.is_def_eq(ai, bi)? { |
| 1370 | return Ok(false); |
| 1371 | } |
| 1372 | } |
| 1373 | Ok(true) |
no test coverage detected