Alphabetical keyword list

• action: declaration of an action
• after: declaration of a mixin
• alias: declaration of an alias
• apply: judgment application in a proof
• around: abbreviation for a pair of anonymous mixins
• assert: statement asserting a proposition
• assume: statement of an assumption; also a tactic
• attribute: declaration of an attribute
• autoinstance: declaration of an autoinstance
• axiom: declaration of an axiom
• before: declaration of a mixin
• call: statement invoking an action
• class: synonym for module
• concept: related to "concept graphs", undocumented
• conjecture: obsolete keyword from earlier Ivy versions
• constructor: undocumented
• decreases: ranking function of a loop
• defergoal: tactic that defers a proof goal
• definition: declaration of a definition
• delegate: related to preconditions, unclear.
• derived: related to "derived relations", unclear.
• destructor: declaration of a private destructor
• else: negative branch of a conditional statement
• ensure: postcondition
• ensures: obsolete keyword from earlier Ivy versions
• entry: obsolete keyword from earlier Ivy versions
• eventually: term in a temporal property
• execute: synonym for mixin (declaring a mixin)
• exists: existential quantifier for an expression
• explicit: qualifier for primitive judgments
• export: marks an action as exported to the environment
• extract: indicates which isolates should be subject to code extraction
• false: primitive proposition
• finite: undocumented
• forall: universal quantifier for an expression
• forget: tactic that forgets a declaration from premises
• fresh: adds a freshness qualifier to a schema premise
• from: part of "pattern based updates", undocumented
• function: declaration of a function
• ghost: indicates that a type is to be considered ghost code
• globally: term in a temporal property
• if: positive branch of a conditional statement
• implement: provides an implementation of an abstract action
• implementation: marks declarations as "implementation" in isolate verification
• import: marks an action as imported from the environment
• in: indicates chosen value in choice function
• include: incorporates another Ivy source file's declarations into the current file
• individual: declaration of an individual
• init: mixin declaration for an initializer
• instance: declaration of an object that instantiates a module, also a tactic that does explicit quantifier instantiation in a proof
• instantiate: synonym for instance
• interpret: primitive judgment of theory instantiation
• invariant: primitive judgment of an invariant
• isa: tests whether type is-a specific variant (subtype)
• isolate: declares a special kind of object verified in isolation from others
• let: binds a local symbol in a proof
• local: binds a logical variable in an action
• macro: declaration of a macro action
• match: obsolete keyword from earlier Ivy versions
• maximizing: qualifier for nondeterministic choice
• method: synonym for action (declaring an action)
• minimizing: qualifier for nondeterministic choice
• mixin: declaration of a mixin
• mixord: declaration of a "mixin order relation"; undocumented
• modifies: solete keyword from earlier Ivy versions
• module: declaration of a module
• named: introduces a named existential
• null: obsolete keyword from earlier Ivy versions
• object: declaration of a singleton object
• of: indicates type of variant
• old: allows referring to an old value in an action
• parameter: declaration of a parameter
• params: part of "pattern based updates", undocumented
• private: marks declarations as "private" in isolate verification
• progress: obsolete keyword from earlier Ivy versions
• proof: optionally provides a proof following a property or theorem
• property: declares a property
• relation: declares a relation
• rely: obsolete keyword from earlier Ivy versions
• require: precondition
• requires: obsolete keyword from earlier Ivy versions
• returns: qualifier of an action indicating its return type
• scenario: part of "scenario mixins", undocumented
• schema: declaration of an axiom schema
• set: obsolete keyword from earlier Ivy versions
• showgoals: tactic that prints current proof goals
• some: selects a value with nondeterministic choice
• specification: marks declarations as "specification" in isolate verification
• spoil: undocumented tactic
• state: obsolete keyword from earlier Ivy versions
• struct: provides a struct definition for a type
• tactic: invokes an extended tactic in a proof
• temporal: declaration of a temporal property
• theorem: declares a theorem
• this: alias for the innermost enclosing module
• thunk: defines a thunk
• true: primitive proposition
• trusted: marks an isolate as verified without proof
• type: primitive judgment introducing a type
• unfold: tactic for unfolding a definition
• update: part of "pattern based updates", undocumented
• using: undocumented, similar to include
• var: primitive judgment introducing a declared variable; in an action, synonymous with a local variable
• variant: declaration of a variant
• while: loop statement
• with: qualifier for isolate combination, in isolate declarations

Categorical

• Logical judgment declarations

  • type introduces a type
  • function introduces a function
  • relation introduces a relation
  • individual introduces an individual
  • var declares a declared variable
  • axiom introduces an axiom or axiom schema (a proposition without proof)
  • property introduces a property (a proposition with proof)
  • theorem introduces a theorem (a schema for properties)
  • definition introduces a definition, a special-case axiom
  • interpret performs theory instantiation

• Other declarations

  • module introduces a module
  • instantiate instantiates a module into an object
  • object introduces a singleton module instantiation
  • isolate introduces an isolate
  • proof optionally provides a proof following a property or theorem
  • action introduces an action
  • before and after introduce mixins
  • private, specification and implementation are visibility qualifiers
  • implement implements the body of an action

• Statements inside actions

  • ensure is a postcondition: asserts a proposition and blames the current action if it fails
  • require is a precondition: asserts a proposition and blames the caller if it fails (or else assumes the environment guarantees it)
  • assume introduces an assumption
  • assert introduces an assertion
  • call calls another action
  • if / else: form a conditional
  • while forms a loop
  • var declares a local variable

• Tactics within proofs

  • apply instantiates a compound judgment and supplies premises to it
  • instantiate instantiates a primitive judgment and performs explicit quantifier instantiation
  • tactic skolemize performs skolemization