package arend.compiled

Get desktop application:
View/edit binary Protocol Buffers messages

Used in: Definition.DataData.Constructor, Definition.FunctionData

• oneof kind

  • ElimBody elim_body = 1

  • Body.IntervalElim interval_elim = 2

  • Expression expression = 3

Used in: IntervalElim

• optional Expression left = 1

• optional Expression right = 2

Used in: Body

• repeated ExpressionPair case = 1

• optional ElimBody otherwise = 2

Used in: ModuleCallTargets

• string name = 1

• int32 index = 2

• repeated CallTargetTree subtree = 3

Used in: Group

• oneof definition_data

  • Definition.ClassData class = 1

  • Definition.DataData data = 2

  • Definition.FunctionData function = 3

  • Definition.DConstructorData constructor = 4

  • Definition.MetaData meta = 5

• UniverseKind universe_kind = 6

• map<string, bytes> user_data = 7

• repeated int32 meta_ref = 8

• int32 p_levels_parent = 9

• int32 h_levels_parent = 10

• bool p_levels_derived = 11

• bool h_levels_derived = 12

• repeated Definition.LevelParameter level_param = 13

• bool is_std_levels = 14

• repeated Definition.ParameterOriginalDef parameter_original_def = 15

• repeated int32 axiom = 16

• bool no_errors = 17

Used in: Definition

• repeated int32 super_class_ref = 1

• repeated ClassData.Field personal_field = 2

• repeated int32 field_ref = 3

• map<int32, Expression.Abs> implementations = 4

• map<int32, DefaultData> defaults = 17

• map<int32, RefList> default_dependencies = 15

• map<int32, RefList> default_impl_dependencies = 16

• int32 coercing_field_ref = 5

• optional Sort sort = 6

• bool is_record = 7

• optional CoerceData coerce_data = 8

• repeated int32 good_field = 9

• repeated int32 type_class_field = 10

• repeated ClassParametersLevel parameters_level = 11

• map<int32, OverriddenData> overridden_field = 23

• repeated int32 covariant_field = 20

• int32 squasher = 13

• map<int32, Levels> super_levels = 19

• UniverseKind base_universe_kind = 21

• repeated int32 omega_field = 22

Used in: ClassData

• optional Referable referable = 1

• optional Expression.Pi type = 2

• optional Expression type_level = 3

• int32 result_type_level = 14

• int32 number_of_parameters = 4

• bool isExplicit = 6

• bool isParameter = 7

• bool isRealParameter = 13

• bool isProperty = 8

• bool isHideable = 9

• UniverseKind universe_kind = 11

• map<string, bytes> user_data = 12

Used in: ClassData

• optional ParametersLevel parameters_level = 1

• repeated int32 field = 2

• bool is_strict = 3

• repeated ClassParametersLevel.ClassExtSig class_ext_sig = 4

Used in: ClassParametersLevel

• int32 class_def = 1

• repeated int32 field = 2

Used in: ClassData, DataData

• repeated CoerceData.Element coerce_from = 1

• repeated CoerceData.Element coerce_to = 2

Used in: Element

• PI = 0

• SIGMA = 1

• UNIVERSE = 2

• ANY = 3

Used in: Element

• int32 classifying_def = 1

Used in: CoerceData

• oneof key

  • DefinitionKey definition_key = 3

  • ConstantKey constant_key = 4

• repeated int32 coercing_def = 2

Used in: Definition

• optional FunctionData function = 1

• int32 number_of_parameters = 2

• optional DPattern pattern = 3

Used in: DConstructorData, DPattern.Constructor

• oneof kind

  • int32 binding = 1

  • DPattern.Constructor constructor = 2

Used in: DPattern

• optional Expression expression = 1

• repeated DPattern pattern = 2

Used in: Definition

• repeated Telescope param = 1

• repeated int32 parameters_typechecking_order = 2

• repeated bool good_this_parameters = 3

• repeated TypeClassParameterKind type_class_parameters = 4

• repeated int32 recursive_definition = 14

• optional Sort sort = 5

• repeated DataData.Constructor constructor = 6

• int32 truncated_level = 15

• bool is_squashed = 8

• int32 squasher = 10

• repeated bool covariant_parameter = 11

• optional CoerceData coerce_data = 12

• repeated ParametersLevel parameters_levels = 13

• bool has_enclosing_class = 16

• repeated bool omega_parameter = 19

Used in: DataData

• optional Referable referable = 1

• repeated Pattern pattern = 2

• repeated Telescope param = 3

• repeated int32 parameters_typechecking_order = 4

• repeated bool good_this_parameters = 5

• repeated TypeClassParameterKind type_class_parameters = 6

• optional Body conditions = 8

• map<string, bytes> user_data = 9

• int32 recursive_parameter = 10

• repeated bool strict_parameters = 11

Used in: ClassData

• optional Expression.Abs expr = 1

• bool is_func = 2

Used in: Definition, DConstructorData

• repeated Telescope param = 1

• repeated int32 parameters_typechecking_order = 2

• repeated bool good_this_parameters = 3

• repeated TypeClassParameterKind type_class_parameters = 4

• repeated int32 recursive_definition = 12

• optional Expression type = 5

• optional Expression type_level = 6

• optional Body body = 7

• FunctionKind kind = 8

• int32 visible_parameter = 9

• repeated ParametersLevel parameters_levels = 10

• FunctionData.HiddenStatus body_hidden_status = 16

• bool has_enclosing_class = 13

• repeated bool strict_parameters = 15

• repeated bool omega_parameter = 19

Used in: FunctionData

• NOT_HIDDEN = 0

• HIDDEN = 1

• REALLY_HIDDEN = 2

Used in: FunctionData

• FUNC = 0

• SFUNC = 1

• LEMMA = 2

• TYPE = 6

• INSTANCE = 3

• COCLAUSE = 4

• COCLAUSE_LEMMA = 5

Used in: Definition, MetaData

• bool is_plevel = 1

• string name = 2

• int32 size = 3

• int32 index = 4

Used in: Definition

• repeated LevelParameter level_param = 1

• repeated Telescope param = 2

• repeated bool typed_param = 3

Used in: ClassData

• optional Expression.Pi type = 1

• int32 original_class = 2

Used in: Definition

• int32 index = 1

• int32 definition = 2

Used in: ClassParametersLevel, DataData, FunctionData

• bool hasParameters = 1

• repeated Telescope parameter = 2

• int32 level = 3

Used in: ClassData

• repeated int32 ref = 1

Used in: DataData, DataData.Constructor, FunctionData

• YES = 0

• NO = 1

• ONLY_LOCAL = 3

Used in: Body, Body.IntervalElim, Expression.Case

• repeated ElimClause clause = 1

• optional ElimTree elim_tree = 2

Used in: ElimBody

• repeated Pattern pattern = 1

• optional Expression expression = 2

Used in: ElimBody, ElimTree.Branch, ElimTree.Branch.ArrayClause, ElimTree.Branch.SingleConstructorClause

• int32 skip = 1

• oneof kind

  • ElimTree.Leaf leaf = 2

  • ElimTree.Branch branch = 3

Used in: ElimTree

• map<int32, ElimTree> clauses = 1

• optional Branch.SingleConstructorClause single_clause = 2

• optional Branch.ArrayClause array_clause = 4

• bool keep_con_call = 3

Used in: Branch

• bool with_elements_type = 1

• bool with_length = 4

• optional ElimTree emptyElimTree = 2

• optional ElimTree consElimTree = 3

Used in: Branch

• oneof kind

  • SingleConstructorClause.Tuple tuple = 1

  • SingleConstructorClause.Class class = 2

  • SingleConstructorClause.Idp idp = 3

• optional ElimTree elim_tree = 4

Used in: SingleConstructorClause

• int32 class_ref = 1

• optional Levels levels = 4

• repeated int32 field = 3

Used in: SingleConstructorClause

(message has no fields)

Used in: SingleConstructorClause

• int32 length = 1

• repeated int32 property_index = 2

Used in: ElimTree

• repeated int32 index = 1

• bool has_indices = 2

• int32 clause_index = 3

Used in: Body, Body.ExpressionPair, Definition.ClassData.Field, Definition.DPattern.Constructor, Definition.FunctionData, ElimClause, Expression.Abs, Expression.App, Expression.Array, Expression.At, Expression.Box, Expression.Case, Expression.ClassCall.ImplEntry, Expression.ConCall, Expression.DataCall, Expression.Error, Expression.EvaluatingReference, Expression.FieldCall, Expression.FunCall, Expression.Lam, Expression.Let, Expression.Let.Clause, Expression.New, Expression.PEval, Expression.Path, Expression.Pi, Expression.Proj, Expression.Tuple, Expression.TypeConstructor, Expression.TypeDestructor, Pattern.ExpressionConstructor, Pattern.ExpressionConstructor.ArrayData, Type, TypedBinding

• oneof kind

  • Expression.App app = 1

  • Expression.ClassCall class_call = 2

  • Expression.ConCalls con_calls = 21

  • Expression.DataCall data_call = 4

  • Expression.Error error = 5

  • Expression.FieldCall field_call = 6

  • Expression.FunCall fun_call = 7

  • Expression.Lam lam = 8

  • Expression.Let let = 9

  • Expression.Case case = 10

  • Expression.New new = 11

  • Expression.Pi pi = 12

  • Expression.Proj proj = 13

  • Expression.Reference reference = 14

  • Expression.EvaluatingReference evaluating_reference = 26

  • Expression.Sigma sigma = 15

  • Expression.Tuple tuple = 16

  • Expression.Universe universe = 17

  • Expression.SmallInteger small_integer = 18

  • Expression.BigInteger big_integer = 19

  • Expression.String string = 30

  • Expression.PEval pEval = 20

  • Expression.Box box = 29

  • Expression.TypeConstructor type_constructor = 27

  • Expression.TypeDestructor type_destructor = 28

  • Expression.Array array = 23

  • Expression.Path path = 24

  • Expression.At at = 25

Used in: Definition.ClassData, Definition.DefaultData

• optional TypedBinding binding = 1

• optional Expression expression = 2

Used in: Expression

• optional Expression function = 1

• optional Expression argument = 2

• bool is_explicit = 3

Used in: Expression

• optional Level pLevel = 5

• optional Level hLevel = 6

• optional Expression elementsType = 2

• repeated Expression element = 3

• optional Expression tail = 4

Used in: Expression

• optional Expression pathArgument = 3

• optional Expression intervalArgument = 4

Used in: Expression

• bytes value = 1

Used in: Expression

• optional Expression expression = 1

• optional Expression type = 2

Used in: Expression

• bool isSFunc = 1

• optional ElimBody elim_body = 2

• repeated Telescope param = 3

• optional Expression result_type = 4

• optional Expression result_type_level = 5

• repeated Expression argument = 6

Used in: Expression, New, Pattern.ExpressionConstructor.ArrayData

• int32 class_ref = 1

• optional Levels levels = 7

• repeated ClassCall.ImplEntry field_impl = 8

• optional Sort sort = 5

• UniverseKind universe_kind = 6

Used in: ClassCall

• int32 field = 1

• optional Expression impl = 2

Used in: ConCalls

• int32 constructor_ref = 1

• optional Levels levels = 7

• repeated Expression datatype_argument = 4

• repeated Expression argument = 5

• int32 recursive_param = 6

Used in: Expression

• repeated ConCall con_call = 1

Used in: Expression

• int32 data_ref = 1

• optional Levels levels = 5

• repeated Expression argument = 4

Used in: Expression

• optional Expression expression = 1

• bool is_goal = 2

• string goal_name = 4

• bool use_expression = 3

Used in: Expression

• string name = 1

• optional Expression expression = 2

Used in: Expression

• int32 field_ref = 1

• optional Expression expression = 4

Used in: Expression

• int32 fun_ref = 1

• optional Levels levels = 5

• repeated Expression argument = 4

Used in: Expression

• optional Sort resultSort = 1

• optional Telescope param = 2

• optional Expression body = 3

Used in: Expression

• bool is_strict = 1

• repeated Let.Clause clause = 2

• optional Let.Pattern pattern = 3

• optional Expression expression = 4

Used in: Let

• bool is_let = 4

• string name = 1

• optional Pattern pattern = 2

• optional Expression expression = 3

Used in: Let, Clause

• Pattern.Kind kind = 1

• string name = 2

• repeated int32 field = 3

• repeated Pattern pattern = 4

Used in: Pattern

• NAME = 0

• TUPLE = 1

• RECORD = 2

Used in: Expression

• optional ClassCall class_call = 1

• optional Expression renew = 2

Used in: Expression

• optional Expression expression = 1

Used in: Expression

• optional Level pLevel = 1

• optional Level hLevel = 2

• optional Expression argumentType = 3

• optional Expression argument = 4

Used in: Definition.ClassData.Field, Definition.OverriddenData, Expression

• optional Sort resultSort = 1

• optional Telescope param = 2

• optional Expression codomain = 3

Used in: Expression

• optional Expression expression = 1

• int32 field = 2

• bool boxed = 3

Used in: Expression

• int32 binding_ref = 1

Used in: Expression, Tuple

• optional Level pLevel = 1

• optional Level hLevel = 2

• repeated Telescope param = 3

Used in: Expression

• int32 value = 1

Used in: Expression

• string value = 1

Used in: Expression

• repeated Expression field = 1

• optional Sigma type = 2

Used in: Expression

• int32 fun_ref = 1

• optional Levels levels = 8

• int32 clause_index = 4

• repeated Expression clause_argument = 5

• optional Expression argument = 6

Used in: Expression

• int32 fun_ref = 1

• optional Expression argument = 6

Used in: Expression

• optional Sort sort = 1

Used in: Module

• optional Referable referable = 1

• optional Definition definition = 2

• repeated Group subgroup = 3

• repeated Group dynamic_subgroup = 4

• repeated int32 invisible_internal_referable = 5

Used in: Expression.Array, Expression.Path, Expression.Sigma, Levels, Sort

• int32 constant = 1

• int32 max_constant = 3

• int32 variable = 4

Used in: Definition.ClassData, ElimTree.Branch.SingleConstructorClause.Class, Expression.ClassCall, Expression.ConCall, Expression.DataCall, Expression.FunCall, Expression.TypeConstructor, Pattern.ExpressionConstructor.ArrayData

• repeated Level pLevel = 1

• repeated Level hLevel = 2

• bool is_std = 3

• int32 version = 4

• bool complete = 3

• optional Group group = 1

• repeated ModuleCallTargets module_call_targets = 2

Used in: Module

• repeated string name = 1

• repeated CallTargetTree call_target_tree = 2

Used in: Definition.DataData.Constructor, ElimClause, Pattern.Constructor, Pattern.ExpressionConstructor

• oneof kind

  • Pattern.Binding binding = 1

  • Pattern.ExpressionConstructor expression_constructor = 2

  • Pattern.Constructor constructor = 3

  • Pattern.Empty empty = 4

Used in: Pattern

• optional SingleParameter var = 1

Used in: Pattern

• int32 definition = 1

• repeated Pattern pattern = 2

Used in: Pattern

• optional SingleParameter var = 1

Used in: Pattern

• optional Expression expression = 1

• repeated Pattern pattern = 2

• optional ExpressionConstructor.ArrayData array_data = 3

Used in: ExpressionConstructor

• int32 constructor = 1

• optional Levels levels = 2

• optional Expression length = 3

• optional Expression elements_type = 4

• optional Expression.ClassCall class_call = 5

• int32 this_binding = 6

• ArrayData.Kind kind = 7

Used in: ArrayData

• EMPTY = 0

• NON_EMPTY = 1

• UNKNOWN = 2

Used in: Referable

• Precedence.Assoc assoc = 1

• int32 priority = 2

• bool infix = 3

Used in: Precedence

• LEFT = 0

• RIGHT = 1

• NON_ASSOC = 2

Used in: Definition.ClassData.Field, Definition.DataData.Constructor, Group

• string name = 1

• optional Precedence precedence = 2

• int32 index = 3

Used in: Pattern.Binding, Pattern.Empty

• string name = 1

• bool is_not_explicit = 2

• optional Type type = 3

• bool is_hidden = 4

Used in: Definition.ClassData, Definition.DataData, Expression.ClassCall, Expression.Lam, Expression.Pi, Expression.Universe, Type

• optional Level p_level = 1

• optional Level h_level = 2

Used in: Definition.DataData, Definition.DataData.Constructor, Definition.FunctionData, Definition.MetaData, Definition.ParametersLevel, Expression.Case, Expression.Lam, Expression.Pi, Expression.Sigma

• repeated string name = 1

• bool is_not_explicit = 2

• optional Type type = 3

• bool is_hidden = 4

• bool is_property = 5

Used in: SingleParameter, Telescope

• optional Expression expr = 1

• optional Sort sort = 2

Used in: Expression.Abs

• string name = 1

• optional Expression type = 2

Used in: Definition, Definition.ClassData, Definition.ClassData.Field, Expression.ClassCall

• NO_UNIVERSES = 0

• ONLY_COVARIANT = 1

• WITH_UNIVERSES = 2