Build Bool environment with working recursor rules.
()
| 266 | |
| 267 | /// Build Bool environment with working recursor rules. |
| 268 | fn bool_env() -> KEnv<Meta> { |
| 269 | let mut env = KEnv::<Meta>::new(); |
| 270 | let n = "Bool"; |
| 271 | let block_id = mk_id(n); |
| 272 | let false_id = mk_id("Bool.false"); |
| 273 | let true_id = mk_id("Bool.true"); |
| 274 | let rec_id = mk_id("Bool.rec"); |
| 275 | |
| 276 | // Bool : Type |
| 277 | env.insert( |
| 278 | block_id.clone(), |
| 279 | KConst::Indc { |
| 280 | name: mk_name(n), |
| 281 | level_params: vec![], |
| 282 | lvls: 0, |
| 283 | params: 0, |
| 284 | indices: 0, |
| 285 | is_unsafe: false, |
| 286 | block: block_id.clone(), |
| 287 | member_idx: 0, |
| 288 | ty: sort1(), |
| 289 | ctors: vec![false_id.clone(), true_id.clone()], |
| 290 | lean_all: vec![block_id.clone()], |
| 291 | }, |
| 292 | ); |
| 293 | |
| 294 | // Bool.false : Bool |
| 295 | env.insert( |
| 296 | false_id.clone(), |
| 297 | KConst::Ctor { |
| 298 | name: mk_name("Bool.false"), |
| 299 | level_params: vec![], |
| 300 | is_unsafe: false, |
| 301 | lvls: 0, |
| 302 | induct: block_id.clone(), |
| 303 | cidx: 0, |
| 304 | params: 0, |
| 305 | fields: 0, |
| 306 | ty: cnst(n, &[]), |
| 307 | }, |
| 308 | ); |
| 309 | |
| 310 | // Bool.true : Bool |
| 311 | env.insert( |
| 312 | true_id.clone(), |
| 313 | KConst::Ctor { |
| 314 | name: mk_name("Bool.true"), |
| 315 | level_params: vec![], |
| 316 | is_unsafe: false, |
| 317 | lvls: 0, |
| 318 | induct: block_id.clone(), |
| 319 | cidx: 1, |
| 320 | params: 0, |
| 321 | fields: 0, |
| 322 | ty: cnst(n, &[]), |
| 323 | }, |
| 324 | ); |
| 325 |