git.iko.soy/Idris-dev
on master help sign in
Small change to list.idr file removing stray qualified names.
3e3cbfbDominic Mulligan
lib/prelude/list.idr+10−13
compare with master
unifiedsplit
@@ -1,8 +1,5 @@
1module prelude.list
1module prelude.list
2
2
3−import prelude.maybe
4−import builtins
5−
6%access public
3%access public
7
4
8import builtins
5import builtins
@@ -467,59 +464,59 @@ hasAnyNilFalse l = ?hasAnyNilFalseBody
467-- Proofs
464-- Proofs
468--------------------------------------------------------------------------------
465--------------------------------------------------------------------------------
469
466
470−MoreList.lengthAppendStepCase = proof {
467+lengthAppendStepCase = proof {
471 intros;
468 intros;
472 rewrite inductiveHypothesis;
469 rewrite inductiveHypothesis;
473 trivial;
470 trivial;
474}
471}
475
472
476−MoreList.hasAnyNilFalseBody = proof {
473+hasAnyNilFalseBody = proof {
477 intros;
474 intros;
478 rewrite (hasAnyByNilFalse (==) l);
475 rewrite (hasAnyByNilFalse (==) l);
479 trivial;
476 trivial;
480}
477}
481
478
482−MoreList.hasAnyByNilFalseStepCase = proof {
479+hasAnyByNilFalseStepCase = proof {
483 intros;
480 intros;
484 rewrite inductiveHypothesis;
481 rewrite inductiveHypothesis;
485 trivial;
482 trivial;
486}
483}
487
484
488−MoreList.initProof = proof {
485+initProof = proof {
489 intros;
486 intros;
490 trivial;
487 trivial;
491}
488}
492
489
493−MoreList.lastProof = proof {
490+lastProof = proof {
494 intros;
491 intros;
495 trivial;
492 trivial;
496}
493}
497
494
498−MoreList.appendNilRightNeutralStepCase = proof {
495+appendNilRightNeutralStepCase = proof {
499 intros;
496 intros;
500 rewrite inductiveHypothesis;
497 rewrite inductiveHypothesis;
501 trivial;
498 trivial;
502}
499}
503
500
504−MoreList.appendAssociativeStepCase = proof {
501+appendAssociativeStepCase = proof {
505 intros;
502 intros;
506 rewrite inductiveHypothesis;
503 rewrite inductiveHypothesis;
507 trivial;
504 trivial;
508}
505}
509
506
510−MoreList.mapFusionStepCase = proof {
507+mapFusionStepCase = proof {
511 intros;
508 intros;
512 rewrite inductiveHypothesis;
509 rewrite inductiveHypothesis;
513 trivial;
510 trivial;
514}
511}
515
512
516−MoreList.mapDistributesOverAppendStepCase = proof {
513+mapDistributesOverAppendStepCase = proof {
517 intros;
514 intros;
518 rewrite inductiveHypothesis;
515 rewrite inductiveHypothesis;
519 trivial;
516 trivial;
520}
517}
521
518
522−MoreList.mapPreservesLengthStepCase = proof {
519+mapPreservesLengthStepCase = proof {
523 intros;
520 intros;
524 rewrite inductiveHypothesis;
521 rewrite inductiveHypothesis;
525 trivial;
522 trivial;