Skip to content

Fix docs typo (syntax for optional arguments)#59

Open
mdbrnowski wants to merge 1 commit intoleanprover-community:mainfrom
mdbrnowski:main
Open

Fix docs typo (syntax for optional arguments)#59
mdbrnowski wants to merge 1 commit intoleanprover-community:mainfrom
mdbrnowski:main

Conversation

@mdbrnowski
Copy link

The documentation for the tactic currently suggests something like this:

example (x y : Nat) : x = y := by
  plausible (config : {maxSize := 200})

When it clearly should be:

example (x y : Nat) : x = y := by
  plausible (config := {maxSize := 200})

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant