Skip to content

Commit

Permalink
Merge pull request #2 from ocfnash/in_current_file_fix
Browse files Browse the repository at this point in the history
Change `in_current_file` --> `in_current_file'`
  • Loading branch information
PatrickMassot committed Feb 12, 2021
2 parents c6786f7 + 435731d commit fac8a7a
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ but already usable for fun.

## Installation

You need Python 3.6 or later, and Lean 3.4. Make sure the python package
You need Python 3.6 or later, and Lean 3.26. Make sure the python package
manager `pip` is installed. Clone this repository, go to its root directory
and run `pip install .` (using `sudo` if needed). It's also recommended to
install `ipython` for interactive use. Alternatively, if you don't want to mess
Expand Down
2 changes: 1 addition & 1 deletion src/leancrawler/deps.lean
Original file line number Diff line number Diff line change
Expand Up @@ -219,7 +219,7 @@ meta def print_content : tactic unit :=
do curr_env ← get_env,
let decls := curr_env.fold [] list.cons,
let local_decls := decls.filter
(λ x, environment.in_current_file' curr_env (to_name x) && not (to_name x).is_internal),
(λ x, environment.in_current_file curr_env (to_name x) && not (to_name x).is_internal),
local_decls.mmap' (print_item_crawl curr_env)

meta def print_all_content : tactic unit :=
Expand Down

0 comments on commit fac8a7a

Please sign in to comment.