Closed Seasawher closed 1 week ago
open Lean Parser Category -- macro "big_step" e:Aesop.rule_expr : attr => -- `(attr| aesop (rule_sets := [BigStepRules]) $e)