Wildcard for destruct as?

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring

11 stars 6 forks source link

Wildcard for destruct as? #102

Closed jaewooklee93 closed 9 years ago

jaewooklee93 commented 9 years ago

In homework, I tried to write

destruct a1 as [n1|x1|a1_1 a1_2|a1_1 a1_2|a1_1 a1_2]; try destruct n1;

However, I only need n1 and the remaining names are not necessary. Can I just leave them blank? like [n1||||], or is it impossible?

jeehoonkang commented 9 years ago

Blank is good.
If you want to place something, put ?.
Try putting _ and see if what happens :-)

jaewooklee93 commented 9 years ago

I already tried several ways which seem reasonable, but

destruct a1 as [n1||||]; try destruct n1; gave Syntax error: "|" or "]" expected (in [disjunctive_intropattern]). and destruct a1 as [n1|_|_|_|_]; try destruct n1; or destruct a1 as [n1|_|_ _|_ _|_ _]; try destruct n1; gave Error: _ is used in conclusion.

But destruct a1 as [n1|?|?|?|?]; try destruct n1;, you suggested, works well.

jeehoonkang commented 9 years ago

Ah, || is interpreted as Propositional OR. You should give a space like: [| |].

Jeehoon

jaewooklee93 commented 9 years ago

Thank you. I think [n1|?|?|?|?] is preferable, since it may be the most readable.