{ "Copyright header for mathlib": { "scope": "lean4", "prefix": "copyright", "body": [ "/-", "Copyright (c) ${CURRENT_YEAR} $1. All rights reserved.", "Released under Apache 2.0 license as described in the file LICENSE.", "Authors: $1", "-/" ] } }