2323def substituteCore :
2324 (pi unrestricted term : (family CoreTerm) .
2325 (pi unrestricted depth : Nat .
2326 (pi unrestricted replacement : (family CoreTerm) . (family CoreTerm)))) =
2327 (lambda unrestricted term : (family CoreTerm) .
2328 (eliminate
2329 CoreTerm
2330 (lambda unrestricted value : (family CoreTerm) .
2331 (pi unrestricted depth : Nat .
2332 (pi unrestricted replacement : (family CoreTerm) . (family CoreTerm))))
2333 term
2334 (branch
2335 CoreUniverse
2336 level
2337 .
2338 (lambda unrestricted depth : Nat .
2339 (lambda unrestricted replacement : (family CoreTerm) .
2340 (constructor CoreTerm CoreUniverse level))))
2341 (branch
2342 CoreNatural
2343 .
2344 (lambda unrestricted depth : Nat .
2345 (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreNatural))))
2346 (branch
2347 CoreNaturalLiteral
2348 value
2349 .
2350 (lambda unrestricted depth : Nat .
2351 (lambda unrestricted replacement : (family CoreTerm) .
2352 (constructor CoreTerm CoreNaturalLiteral value))))
2353 (branch CoreBound index . (substituteCorePart1 index))
2354 (branch
2355 CorePi
2356 multiplicity
2357 domain
2358 codomain
2359 ih_domain
2360 ih_codomain
2361 .
2362 (substituteCorePart2 multiplicity ih_domain ih_codomain))
2363 (branch
2364 CoreLambda
2365 multiplicity
2366 domain
2367 body
2368 ih_domain
2369 ih_body
2370 .
2371 (lambda unrestricted depth : Nat .
2372 (lambda unrestricted replacement : (family CoreTerm) .
2373 (constructor
2374 CoreTerm
2375 CoreLambda
2376 multiplicity
2377 (ih_domain depth replacement)
2378 (ih_body (succ depth) replacement)))))
2379 (branch
2380 CoreLet
2381 multiplicity
2382 annotation
2383 value
2384 body
2385 ih_annotation
2386 ih_value
2387 ih_body
2388 .
2389 (lambda unrestricted depth : Nat .
2390 (lambda unrestricted replacement : (family CoreTerm) .
2391 (constructor
2392 CoreTerm
2393 CoreLet
2394 multiplicity
2395 (ih_annotation depth replacement)
2396 (ih_value depth replacement)
2397 (ih_body (succ depth) replacement)))))
2398 (branch
2399 CoreApplication
2400 function
2401 argument
2402 ih_function
2403 ih_argument
2404 .
2405 (lambda unrestricted depth : Nat .
2406 (lambda unrestricted replacement : (family CoreTerm) .
2407 (constructor
2408 CoreTerm
2409 CoreApplication
2410 (ih_function depth replacement)
2411 (ih_argument depth replacement)))))
2412 (branch
2413 CoreNaturalArithmetic
2414 operation
2415 function
2416 argument
2417 ih_function
2418 ih_argument
2419 .
2420 (lambda unrestricted depth : Nat .
2421 (lambda unrestricted replacement : (family CoreTerm) .
2422 (constructor
2423 CoreTerm
2424 CoreNaturalArithmetic
2425 operation
2426 (ih_function depth replacement)
2427 (ih_argument depth replacement)))))
2428 (branch
2429 CoreNaturalSuccessor
2430 predecessor
2431 ih_predecessor
2432 .
2433 (lambda unrestricted depth : Nat .
2434 (lambda unrestricted replacement : (family CoreTerm) .
2435 (constructor CoreTerm CoreNaturalSuccessor (ih_predecessor depth replacement)))))
2436 (branch
2437 CoreByte
2438 .
2439 (lambda unrestricted depth : Nat .
2440 (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreByte))))
2441 (branch
2442 CoreByteLiteral
2443 value
2444 .
2445 (lambda unrestricted depth : Nat .
2446 (lambda unrestricted replacement : (family CoreTerm) .
2447 (constructor CoreTerm CoreByteLiteral value))))
2448 (branch
2449 CoreBytes
2450 .
2451 (lambda unrestricted depth : Nat .
2452 (lambda unrestricted replacement : (family CoreTerm) . (constructor CoreTerm CoreBytes))))
2453 (branch
2454 CoreBytesLiteral
2455 value
2456 .
2457 (lambda unrestricted depth : Nat .
2458 (lambda unrestricted replacement : (family CoreTerm) .
2459 (constructor CoreTerm CoreBytesLiteral value))))
2460 (branch
2461 CorePrimitiveTerm
2462 primitive
2463 .
2464 (lambda unrestricted depth : Nat .
2465 (lambda unrestricted replacement : (family CoreTerm) .
2466 (constructor CoreTerm CorePrimitiveTerm primitive))))
2467 (branch
2468 CoreTermSequenceEnd
2469 .
2470 (lambda unrestricted depth : Nat .
2471 (lambda unrestricted replacement : (family CoreTerm) .
2472 (constructor CoreTerm CoreTermSequenceEnd))))
2473 (branch
2474 CoreTermSequenceNext
2475 head
2476 tail
2477 ih_head
2478 ih_tail
2479 .
2480 (lambda unrestricted depth : Nat .
2481 (lambda unrestricted replacement : (family CoreTerm) .
2482 (constructor
2483 CoreTerm
2484 CoreTermSequenceNext
2485 (ih_head depth replacement)
2486 (ih_tail depth replacement)))))
2487 (branch
2488 CoreFamilyApplication
2489 familyName
2490 arguments
2491 ih_arguments
2492 .
2493 (lambda unrestricted depth : Nat .
2494 (lambda unrestricted replacement : (family CoreTerm) .
2495 (constructor CoreTerm CoreFamilyApplication familyName (ih_arguments depth replacement)))))
2496 (branch
2497 CoreConstructorApplication
2498 familyName
2499 constructorName
2500 arguments
2501 ih_arguments
2502 .
2503 (lambda unrestricted depth : Nat .
2504 (lambda unrestricted replacement : (family CoreTerm) .
2505 (constructor
2506 CoreTerm
2507 CoreConstructorApplication
2508 familyName
2509 constructorName
2510 (ih_arguments depth replacement)))))
2511 (branch
2512 CoreEliminatorBranch
2513 constructorName
2514 binderCount
2515 body
2516 ih_body
2517 .
2518 (lambda unrestricted depth : Nat .
2519 (lambda unrestricted replacement : (family CoreTerm) .
2520 (constructor
2521 CoreTerm
2522 CoreEliminatorBranch
2523 constructorName
2524 binderCount
2525 (ih_body (naturalAdd depth binderCount) replacement)))))
2526 (branch
2527 CoreEliminator
2528 familyName
2529 motive
2530 scrutinee
2531 branches
2532 ih_motive
2533 ih_scrutinee
2534 ih_branches
2535 .
2536 (lambda unrestricted depth : Nat .
2537 (lambda unrestricted replacement : (family CoreTerm) .
2538 (constructor
2539 CoreTerm
2540 CoreEliminator
2541 familyName
2542 (ih_motive depth replacement)
2543 (ih_scrutinee depth replacement)
2544 (ih_branches depth replacement)))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.