automatically infer proof argument using tactic

Stream: general

[Huỳnh Trần Khanh]

is there a way to make lean infer a proof argument automatically using a tactic? i think i've read about it somewhere but... i can't find that page anymore :cry:

[Huỳnh Trần Khanh]

this is what im trying to achieve:

structure some_value_t :=
(value : \N)
(proof : value < 100)

and i want lean to automatically infer the proof field with the norm_num tactic because i mostly instatiate the structure with a literal value, not a variable

[Huỳnh Trần Khanh]

thanks in advance as usual

[Eric Wieser]

structure some_value_t :=
(value : \N)
(proof : value < 100 . norm_num)

I think

[Huỳnh Trần Khanh]

thanks for the answer. but i got invalid auto_param, 'norm_num' must have type (tactic unit)

[Chris Hughes]

I think it's a bit more complicated than that. The argument after the . has to be a name corresponding to a definition of type tactic unit. The following works

meta def norm_num2 : tactic unit := `[norm_num]

structure some_value_t :=
(value : nat)
(proof : value < 100 . norm_num2)