Mercurial > cpdt > repo
comparison src/Reflection.v @ 554:93471096cdd4
Merge
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 19 Aug 2017 12:14:40 -0400 |
parents | 2c8c693ddaba |
children | a913f19955e2 |
comparison
equal
deleted
inserted
replaced
553:cb81f74d8c92 | 554:93471096cdd4 |
---|---|
671 | 671 |
672 Ltac addToList x xs := | 672 Ltac addToList x xs := |
673 let b := inList x xs in | 673 let b := inList x xs in |
674 match b with | 674 match b with |
675 | true => xs | 675 | true => xs |
676 | false => constr:(x, xs) | 676 | false => constr:((x, xs)) |
677 end. | 677 end. |
678 | 678 |
679 (** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *) | 679 (** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *) |
680 | 680 |
681 Ltac allVars xs e := | 681 Ltac allVars xs e := |
716 | 716 |
717 (** Note that, when we write our own Ltac procedure, we can work directly with the normal [->] operator, rather than needing to introduce a wrapper for it. *) | 717 (** Note that, when we write our own Ltac procedure, we can work directly with the normal [->] operator, rather than needing to introduce a wrapper for it. *) |
718 | 718 |
719 Ltac reifyTerm xs e := | 719 Ltac reifyTerm xs e := |
720 match e with | 720 match e with |
721 | True => constr:Truth' | 721 | True => Truth' |
722 | False => constr:Falsehood' | 722 | False => Falsehood' |
723 | ?e1 /\ ?e2 => | 723 | ?e1 /\ ?e2 => |
724 let p1 := reifyTerm xs e1 in | 724 let p1 := reifyTerm xs e1 in |
725 let p2 := reifyTerm xs e2 in | 725 let p2 := reifyTerm xs e2 in |
726 constr:(And' p1 p2) | 726 constr:(And' p1 p2) |
727 | ?e1 \/ ?e2 => | 727 | ?e1 \/ ?e2 => |