| 287 | Expr::var(0), |
| 288 | ); |
| 289 | let mut buf = Vec::new(); |
| 290 | serialize::put_expr(&expr, &mut buf); |
| 291 | assert_eq!( |
| 292 | buf, |
| 293 | vec![0x73, 0x13, 0x12, 0x11, 0x10], |
| 294 | "App telescope should be [0x73, 0x13, 0x12, 0x11, 0x10]" |
| 295 | ); |
| 296 | } |
| 297 | |
| 298 | #[test] |
| 299 | fn expr_lam_telescope() { |
| 300 | // Lam(t1, Lam(t2, Lam(t3, body))) with all types Sort(0) and body Var(0) |
| 301 | // -> Tag4 { flag: 0x8, size: 3 } + t1 + t2 + t3 + body |
| 302 | // = 0x83 + 0x00 + 0x00 + 0x00 + 0x10 |
| 303 | let ty = Expr::sort(0); |
| 304 | let expr = Expr::lam( |
| 305 | ty.clone(), |
| 306 | Expr::lam(ty.clone(), Expr::lam(ty.clone(), Expr::var(0))), |
| 307 | ); |
| 308 | let mut buf = Vec::new(); |