Mercurial > cpdt > repo
comparison src/Match.v @ 554:93471096cdd4
Merge
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sat, 19 Aug 2017 12:14:40 -0400 |
| parents | 2c8c693ddaba |
| children |
comparison
equal
deleted
inserted
replaced
| 553:cb81f74d8c92 | 554:93471096cdd4 |
|---|---|
| 442 (** Ltac functions can have no implicit arguments. It may seem surprising that we need to pass [T], the carried type of the output list, explicitly. We cannot just use [type of f], because [f] is an Ltac term, not a Gallina term, and Ltac programs are dynamically typed. The function [f] could use very syntactic methods to decide to return differently typed terms for different inputs. We also could not replace [constr:(@nil T)] with [constr:nil], because we have no strongly typed context to use to infer the parameter to [nil]. Luckily, we do have sufficient context within [constr:(x' :: ls'')]. | 442 (** Ltac functions can have no implicit arguments. It may seem surprising that we need to pass [T], the carried type of the output list, explicitly. We cannot just use [type of f], because [f] is an Ltac term, not a Gallina term, and Ltac programs are dynamically typed. The function [f] could use very syntactic methods to decide to return differently typed terms for different inputs. We also could not replace [constr:(@nil T)] with [constr:nil], because we have no strongly typed context to use to infer the parameter to [nil]. Luckily, we do have sufficient context within [constr:(x' :: ls'')]. |
| 443 | 443 |
| 444 Sometimes we need to employ the opposite direction of "nonterminal escape," when we want to pass a complicated tactic expression as an argument to another tactic, as we might want to do in invoking %\coqdocvar{%#<tt>#map#</tt>#%}%. *) | 444 Sometimes we need to employ the opposite direction of "nonterminal escape," when we want to pass a complicated tactic expression as an argument to another tactic, as we might want to do in invoking %\coqdocvar{%#<tt>#map#</tt>#%}%. *) |
| 445 | 445 |
| 446 Goal False. | 446 Goal False. |
| 447 let ls := map (nat * nat)%type ltac:(fun x => constr:(x, x)) (1 :: 2 :: 3 :: nil) in | 447 let ls := map (nat * nat)%type ltac:(fun x => constr:((x, x))) (1 :: 2 :: 3 :: nil) in |
| 448 pose ls. | 448 pose ls. |
| 449 (** [[ | 449 (** [[ |
| 450 l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat) | 450 l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat) |
| 451 ============================ | 451 ============================ |
| 452 False | 452 False |