1364def inspectNamedCoreVariable =
1365 (lambda unrestricted term : (family NamedCoreTerm) .
1366 (eliminate
1367 NamedCoreTerm
1368 (lambda unrestricted value : (family NamedCoreTerm) . (family NamedCoreVariableInspection))
1369 term
1370 (branch
1371 NamedCoreUniverse
1372 level
1373 .
1374 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1375 (branch
1376 NamedCoreNatural
1377 .
1378 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1379 (branch
1380 NamedCoreNaturalLiteral
1381 value
1382 .
1383 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1384 (branch
1385 NamedCoreVariable
1386 identifier
1387 .
1388 (constructor NamedCoreVariableInspection NamedCoreVariableFound identifier))
1389 (branch
1390 NamedCorePi
1391 multiplicity
1392 binder
1393 domain
1394 codomain
1395 ih_domain
1396 ih_codomain
1397 .
1398 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1399 (branch
1400 NamedCoreLambda
1401 multiplicity
1402 binder
1403 domain
1404 body
1405 ih_domain
1406 ih_body
1407 .
1408 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1409 (branch
1410 NamedCoreLet
1411 multiplicity
1412 binder
1413 annotation
1414 value
1415 body
1416 ih_annotation
1417 ih_value
1418 ih_body
1419 .
1420 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1421 (branch
1422 NamedCoreApplication
1423 function
1424 argument
1425 ih_function
1426 ih_argument
1427 .
1428 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1429 (branch
1430 NamedCoreNaturalArithmetic
1431 operation
1432 function
1433 argument
1434 ih_function
1435 ih_argument
1436 .
1437 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1438 (branch
1439 NamedCoreNaturalSuccessor
1440 predecessor
1441 ih_predecessor
1442 .
1443 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1444 (branch NamedCoreByte . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1445 (branch
1446 NamedCoreByteLiteral
1447 value
1448 .
1449 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1450 (branch NamedCoreBytes . (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1451 (branch
1452 NamedCoreBytesLiteral
1453 value
1454 .
1455 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1456 (branch
1457 NamedCoreTermSequenceEnd
1458 .
1459 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1460 (branch
1461 NamedCoreTermSequenceNext
1462 head
1463 tail
1464 ih_head
1465 ih_tail
1466 .
1467 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1468 (branch
1469 NamedCoreFamilyApplication
1470 familyName
1471 arguments
1472 ih_arguments
1473 .
1474 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1475 (branch
1476 NamedCoreConstructorApplication
1477 familyName
1478 constructorName
1479 arguments
1480 ih_arguments
1481 .
1482 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1483 (branch
1484 NamedCoreEliminatorBranch
1485 constructorName
1486 binderNames
1487 body
1488 ih_binderNames
1489 ih_body
1490 .
1491 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))
1492 (branch
1493 NamedCoreEliminator
1494 familyName
1495 motive
1496 scrutinee
1497 branches
1498 ih_motive
1499 ih_scrutinee
1500 ih_branches
1501 .
1502 (constructor NamedCoreVariableInspection NamedCoreTermIsNotVariable))))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.