Skip to content

Commit

Permalink
doc: fix option name (leanprover#5150)
Browse files Browse the repository at this point in the history
Small typo fix. I don't believe there is an `autoBoundImplicitLocal`
option.
  • Loading branch information
Vtec234 authored and tobiasgrosser committed Aug 26, 2024
1 parent d95dd37 commit 7a9411c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Lean/Elab/AutoBound.lean
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ register_builtin_option autoImplicit : Bool := {

register_builtin_option relaxedAutoImplicit : Bool := {
defValue := true
descr := "When \"relaxed\" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see optin `autoBoundImplicitLocal`."
descr := "When \"relaxed\" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see option `autoImplicit`)."
}


Expand Down

0 comments on commit 7a9411c

Please sign in to comment.