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