Documentation
VCVio
.
ProgramLogic
.
Tactics
.
Common
.
Suggestions
Search
return to top
source
Imports
Init
Mathlib.Tactic.TryThis
Imported by
OracleComp
.
ProgramLogic
.
addTryThisTextSuggestion
VCGen Suggestions
#
Helpers for attaching
Try this
suggestions to tactic diagnostics.
source
def
OracleComp
.
ProgramLogic
.
addTryThisTextSuggestion
(
ref
:
Lean.Syntax
)
(
text
:
String
)
:
Lean.MetaM
Unit
Instances For