mathlib

mathlib copied to clipboard

E.g.

import tactic.basic
reserve notation `#file_decls`

-- examples
lemma bar (n : ℕ) (h1 : 0 < n) : 0 < n := sorry
lemma baz (n : ℕ) : 0 < n + 1 := sorry

open tactic
setup_tactic_parser
meta def file_decls : tactic (list (name × expr)) := do
  e ← get_env,
  let l := e.filter (λ d, e.in_current_file d.to_name),
  return (l.map (λ d, ⟨d.to_name, d.type⟩))
@[user_command] meta def file_cmd (_ : parse $ tk "#file_decls") : lean.parser unit :=
trace file_decls.

#file_decls