Remove deprecated functions, add docstring #337

	name: Lint Style

	on:
	push:
	branches: ["main"] # Trigger the workflow on pushes to the "main" branch (replace "main" with your default branch if different)
	pull_request:
	branches: ["main"] # Trigger the workflow on pull requests targeting the "main" branch (replace "main" with your default branch if different)
	workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface

	# Set permissions for the workflow
	permissions:
	contents: read # Grant read access to repository contents
	pages: write # Grant write access to GitHub Pages
	id-token: write # Grant write access to ID tokens

	jobs:
	style_lint:
	runs-on: ubuntu-latest
	steps:
	- name: Check for long lines
	if: always() # Ensure the step runs regardless of the success or failure of previous steps
	run: \|
	# Find Lean files with lines longer than 100 characters, excluding URLs
	! (find expdb -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; \| grep -v -E 'https?://')

	- name: Don't 'import Mathlib', use precise imports
	if: always() # Ensure the step runs regardless of the success or failure of previous steps
	run: \|
	# Find and disallow any file that imports the entire Mathlib, encouraging precise imports instead
	! (find expdb -name "*.lean" -type f -print0 \| xargs -0 grep -E -n '^import Mathlib$')

Provide feedback