refactor: move visibility/unsafe modifiers after alloy c extern

tydeu · Mar 10, 2024 · 6761a8c · 6761a8c
1 parent 5ae885f
commit 6761a8c
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/Alloy/C/ExternDef.lean b/Alloy/C/ExternDef.lean
@@ -24,13 +24,13 @@ alloy c section LEAN_EXPORT uint32_t alloy_foo(uint32_t x) {...}
 ```
 -/
 scoped syntax (name := externDecl)
-(docComment)? (Term.attributes)? (visibility)? «unsafe»?
-"alloy " &"c " &"extern " (str)? "def " declId binders " : " term " := " stmtSeq
+(docComment)? (Term.attributes)?  "alloy " &"c " &"extern " (str)?
+(visibility)? «unsafe»? "def " declId binders " : " term " := " stmtSeq
 : command
 
 elab_rules : command
-| `(externDecl| $[$doc?]? $[$attrs?]? $[$vis?]? $[unsafe%$uTk?]?
-  alloy c extern%$exTk $[$sym?]? def $id $bs* : $ty := $stmts*) => do
+| `(externDecl| $[$doc?]? $[$attrs?]? alloy c extern%$exTk $[$sym?]?
+  $[$vis?]? $[unsafe%$uTk?]? def $id $bs* : $ty := $stmts*) => do
   let cmd ← `($[$doc?]? $[$attrs?]? $[$vis?]? noncomputable $[unsafe%$uTk?]? opaque $id $[$bs]* : $ty)
   withMacroExpansion (← getRef) cmd <| elabCommand cmd
   let bvs ← liftMacroM <| bs.concatMapM matchBinder