ArendBundle.properties

arend.import.fix=Fix import
arend.import.replaceWithShortName=Replace with short name
arend.import.hide=Hide import
arend.import.fixMisplaced=Fix misplaced import
arend.import.rename=Rename import

arend.pattern.doMatching=Do pattern matching on the stuck variable
arend.pattern.makeExplicit=Make pattern explicit
arend.pattern.replaceWithConstructors=Replace with expected pattern constructors
arend.pattern.split=Split atomic pattern
arend.pattern.removeAs=Remove \\as-pattern
arend.pattern.remove=Remove redundant patterns

arend.clause.implement=Implement missing clauses
arend.clause.removeRedundant=Remove redundant clause
arend.clause.removeRedundantRHS=Remove redundant clause's right-hand side

arend.coClause.implementMissing=Implement missing fields
arend.coClause.implementParentFields=Implement fields of {0}
arend.coClause.removeRedundant=Remove redundant coclause
arend.coClause.replaceWithEmptyImplementation=Replace {?} with empty implementation of the class
arend.coClause.changeArgumentExplicitness=Change Argument Explicitness
arend.coClause.changeArgumentExplicitness.question1=Some of the usages could not have been parsed correctly, so the refactoring might break them. Would you like to continue anyway?

arend.instance.addLocalInstance=Add local instance
arend.instance.replaceWithLocalInstance=Replace local parameter with a local instance
arend.instance.importInstance=Add instance import

arend.expression.swapInfixArguments=Swap infix operator arguments
arend.expression.wrapInGoal=Wrap selected into a goal
arend.expression.fillGoal=Fill goal
arend.expression.replaceWithWHNF=Replace with Weak Head Normal Form
arend.expression.replaceMetaWithResult=Replace meta with result
arend.expression.addClarifyingParentheses=Add clarifying parentheses
arend.expression.removeLevel=Remove level
arend.expression.removeClarifyingParentheses=Remove clarifying parentheses
arend.expression.clarifyingParens.processingFailed=Failed to process binary operator
arend.expression.clarifyingParens.unexpectedUseOfImplicitArgs=Unexpected use of implicit arguments after explicit ones
arend.show.type.progress=Computing type representation...

arend.inspection.redundant.parameter.message=Replace the redundant parameter with _
arend.inspection.redundant.parentheses.name=Redundant parentheses
arend.inspection.redundant.parentheses.message=Redundant parentheses
arend.unwrap.parentheses.fix=Unwrap parentheses

arend.inspection.unused.import=Unused import
arend.inspection.unused.import.message.unused.import.0=Import ''{0}'' is not used
arend.inspection.unused.import.message.unused.import=Import is not used
arend.inspection.unused.import.message.unused.open.0=No definitions from ''{0}'' are used
arend.inspection.unused.import.message.unused.open=No definitions from this module are used
arend.inspection.unused.import.message.unused.definition.0=Definition ''{0}'' is not used anywhere
arend.inspection.unused.import.message.unused.definition=Definition is not used anywhere
arend.inspection.name.shadowed=Name ''{0}'' shadowed
arend.inspection.parameter.redundant=The parameter ''{0}'' is redundant
arend.inspection.infix.partially.prefix.form=One explicit argument is to the right of the infix definition with two explicit arguments
arend.inspection.remove.letBinding=Remove unused the let binding
arend.inspection.remove.letBinding.message=The let binding is not used

arend.generate.function=Generate function
arend.generate.function.from.goal=Generate function from goal
arend.generate.function.from.expression=Extract expression to function
arend.create.let.binding=Create \\let-binding
arend.create.let.binding.expression.to.wrap=Expression to Wrap
arend.replace.function.kind=Make into {0}
arend.replace.field.kind=Make into a field
arend.replace.sigma.kind=Remove \\property

arend.startup.loading.arend.modules=Loading Arend modules...

arend.add.information.in.arend.messages=Adding Information...
arend.reveal.implicit.argument=Reveal an implicit argument
arend.hide.implicit.argument=Hide implicit argument
arend.reveal.lambda.parameter.type=Reveal type of lambda parameter
arend.hide.lambda.parameter.type=Hide type of lambda parameter
arend.reveal.type.of.tuple=Reveal type of tuple
arend.hide.type.of.tuple=Hide type of tuple
arend.reveal.proof=Reveal proof
arend.hide.proof=Hide proof

arend.optimize.imports.intention.family.name=Optimize imports
arend.optimize.imports.intention.name=Remove unused \\import and \\open statements

arend.proof.search.include.non.project.locations=Include non-project locations
arend.proof.search.include.test.locations=Include test locations
arend.proof.search.limit.search.results=Interrupt search after {0} matches
arend.proof.search.title=Proof search
arend.proof.search.matches.of=Matches of ''{0}''
arend.proof.search.find.usages.results=Results
arend.proof.search.matches=Matches
arend.proof.search.placeholder=Pattern
arend.proof.search.searching.for.definitions=Searching for Definitions...
arend.proof.search.loading.tooltip=Search is in progress...
arend.proof.search.completed.tooltip=Search is completed
arend.proof.search.syntax.error.in.query=Syntax error in query
arend.proof.search.quick.preview.tip=Press Enter on a selected entry to invoke quick preview
arend.proof.search.go.to.definition.tip=Press {0} on a selected entry to open definition in the editor
arend.proof.search.insert.definition.tip=Press {0} on a selected entry to insert it in your file
arend.proof.search.use.and.tip=Queries like 'foo \\and bar' allow to match only signatures with 'foo' and 'bar' at the same time
arend.proof.search.use.arrow.tip=Queries like 'foo -> bar' allow to specify patterns in parameters
arend.proof.search.show.help=Show Help
arend.proof.search.show.help.description=Open webpage with help

arend.messages.view.no.messages=No messages
arend.messages.view.empty.goal.panel.text=Select a goal to see details
arend.messages.view.empty.error.panel.text=Select an error to see details
arend.messages.view.error.title=Current Error
arend.messages.view.error.tooltip=Shows selected error. This view is cleaned when the error is removed from the file.
arend.messages.view.latest.goal.title=Latest Goal
arend.messages.view.latest.goal.tooltip=Shows selected goal. This view is not cleaned even if the goal is removed from the file.
arend.messages.view.latest.goal.removed.title=Already Removed from the File

arend.libs.description.standard=Arend Standard Library

arend.pin.goal.action.name=Pin Goal
arend.pin.goal.action.description=When the goal is pinned, other goals will not be displayed
arend.pin.error.action.name=Pin Error
arend.pin.error.action.description=When the error is pinned, other errors will not be displayed
arend.clear.goal.action.name=Clear Goal
arend.clear.goal.action.description=Clear goal
arend.show.errors.panel.action.name=Show 'Current Error' Panel
arend.show.errors.panel.action.description=Show 'Current Error' panel
arend.show.goals.in.errors.panel.action.name=Show Goals
arend.show.goals.in.errors.panel.action.description=Show goals
arend.show.implicit.goals.action.name=Show Implicit Goals
arend.show.implicit.goals.action.description=Show implicit goals, i.e. goals that have no corresponding '{?}' element in the source code.

arend.optimize.imports.message.core.used=Imports optimized. All instances were inferred from typechecked expressions.
arend.optimize.imports.message.scope.used=Imports optimized. All visible instances were imported.
arend.code.style.settings.optimize.imports.policy=Optimize Imports Policy
arend.code.style.settings.use.implicit.imports=Import all definitions from modules implicitly (\\hiding will be used to resolve collisions)
arend.code.style.settings.use.explicit.imports=Import all definitions from modules explicitly
arend.code.style.settings.explicit.imports.limit=Limit for explicitly imported definitions (implicit import will be used in case of overflow):
arend.code.style.settings.soft.optimize.imports=Only remove unused imports and opens

arend.tracer.unknown.expression=<unknown>
arend.tracer.no.information=No information
arend.tracer.cannot.find.starting.expression=Cannot find a starting expression, using the first one in the declaration
arend.tracer.declaration.has.errors=Traced declaration has typechecking errors
arend.tracer.nothing.to.trace=No tracing data (nothing to trace)
arend.tracer.command.failed=Command failed
arend.tracer.collecting.tracing.data=Collecting tracing data...
arend.tracer.nothing.to.show=Nothing to show
arend.tracer.cannot.trace.here=Cannot trace here
arend.trace.action.cannot.find.expression=Cannot find declaration or expression at cursor
arend.trace.action.cannot.find.concrete.definition=Cannot find concrete definition corresponding to {0}
arend.trace.next.entry.action.name=Next Trace Entry
arend.trace.next.entry.action.description=Show the next trace entry
arend.trace.prev.entry.action.name=Previous Trace Entry
arend.trace.prev.entry.action.description=Show the previous trace entry
arend.error.wrongCaretPosition=The caret should be positioned at the name of the function to be refactored

arend.argument.explicitness=Make an explicit argument
arend.argument.implicitness=Make an implicit argument
arend.lambda.argument.implicitness=Make an explicit corresponding argument

arend.argument.inference.parameter=Infer parameter

arend.universe.replace=Replace universe
arend.elim.substitute=Add bindings to \\case
arend.return.add=Add \\return keyword
arend.truncated.remove=Remove \\truncated keyword

arend.squashedData.changeKeyword=Change a keyword for squashed data
arend.truncatedData.changeKeyword=Change a keyword for truncated data

arend.field.dependency=Implement the field

arend.disableGroupSource=MarkSourceRootGroup
arend.disableActionExclude=MarkExcludeRoot
arend.disableActionUnmark=UnmarkRoot
arend.icon.modules.binRoot.tooltip=Bin Sources Root
arend.icon.modules.binRoot.unmark=Unmark as Bin Root

arend.click.to.see.diff.link=<Click to see difference>
arend.click.to.see.diff.link.title=Type comparison
arend.click.to.set.cursor.latex=Set the cursor to the incorrect latex formula

arend.refactoring.notTypecheckedMessage.partI.single=Definition {0} might have external parameters.\nNormally, these are inferred by Arend typechecker, however, this definition has not been successfully typechecked.\nRefactoring might be unable to correctly infer its signature.
arend.refactoring.notTypecheckedMessage.partI.multiple=Definitions {0} might have external parameters.\nNormally, these are inferred by Arend typechecker, however, these definitions have not been successfully typechecked.\nRefactoring might be unable to correctly infer their signatures.
arend.refactoring.notTypecheckedMessage.partII=\nFurther manual editing might be required after the refactoring is performed.\n Would you like to proceed anyway?

arend.refactoring.move.canNotLocate=Can not locate target module
arend.refactoring.move.targetEqualsSource=Target module cannot coincide with the source module
arend.refactoring.move.targetSubmoduleSource=Target module cannot be a submodule of the member being moved
arend.refactoring.move.unspecifiedPartOfTheClass=Unspecified part of the class

arend.changeSignature.ambientError=Typechecking error in the expression or its parent
arend.changeSignature.parseError=Unable to parse expression correctly

arend.replaceBrackets=Replace the brackets

arend.updateYamlConfigurationQuestion=Would you like to update the settings from the YAML file?
arend.updateYamlConfiguration=Update
arend.message.fileOutsideSources=The file is located outside of sources
arend.yaml.openDocumentation=Open the documentation