leanprover-community
constant/axiom in sections
section foo
-- invalid declaration, 'constant/axiom' cannot be used in sections
constant foo : Type
end foo
AFAICT this is a restriction without a reason. It would be nice to lift it.
Just guessing, but maybe there is a bad interaction with something like parameters? As far as I know those can only appear inside a section.
The solution there is pretty obvious, though: stick the parameters in the definition as normal, use local notations to pretend the arguments aren't being supplied (as normal) in uses. Really it's no different from the way def foo : Type := sorry would be elaborated.
Looking at the change 4946f5529085a38332110905fa61739e86b504f8 which introduced this restriction, and particularly the doc and test modifications, it looks like this change happened at a time when constant was used differently than we use it now. So I agree there's probably no reason to have this restriction any more.