writing tactics: manipulating names

Stream: general

[Frédéric Le Roux]

I have just written my first tactic "defi" below, which allow to call a lemma whose name is "lemme_defi_something" for rewriting the target, by typing "defi something". I struggled with the different types involved: I had to transform "something" into a string, add to it the prefix "lemme_defi_", then transform this into a name using mk_simple_name, then the name into a constant using mk_const, then the constant into an expression (through a pre-expression).

Is there a more direct way??

Could I have found the command mk_simple_name by a smarter way than searching randomly into the doc ?

meta def defi (name : parse ident) : tactic unit := do let nom_lemme := "lemme_defi_" ++ to_string name, trace ("J'appelle le lemme " ++ nom_lemme), let name := mk_simple_name nom_lemme, name ← mk_const name, expr ← to_expr ```(%%name), do {rewrite_target expr, trace "sens direct"} <|> do {rewrite_target expr {symm := tt}, trace "sens réciproque"}

[Mario Carneiro]

I don't think there is a simpler way. This is a bit of an unusual operation; more common would be to put something in a namespace, that is, lemme_defi.something, in which case you could use <.> for doing the name append operation

[Mario Carneiro]

I don't see the reason for the to_expr step though. mk_const should have already returned an expr

[Mario Carneiro]

I would have found mk_simple_name by looking around in the file where name is defined, which has a number of useful operations on names

[Frédéric Le Roux]

Indeed it works without the to_exprstep. I will consider using a namespace. Thanks!