Могу ли я «карту» «OF» над списком чешуй

Question

Я просто написал этот код:

lemmas gc_step_intros = 
    normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)] 
    normal[OF step.intros(4)] normal[OF step.intros(5)] drop 

где step.intros имеет действительно только 5 лемм. Есть ли удобный способ избежать повторения, т. Е. Что-то, что может выглядеть следующим образом?

lemmas gc_step_intros = normal[OF_EACH step.intros] drop 

Answer 1

Вы можете использовать THEN вместо OF и использовать тот факт, что атрибут применяется ко всем теоремам в списке теорем. Следующие должны делать то, что вы хотите:

lemmas gc_step_intros = step.intros[THEN normal] drop