Module Repl.Command

type t =
  1. | Rename of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. rename_from : Beluga_syntax.Syncom.Identifier.t * [ `Plain | `Hash | `Dollar ];
    3. rename_to : Beluga_syntax.Syncom.Identifier.t * [ `Plain | `Hash | `Dollar ];
    4. level : [ `meta | `comp ];
    }
  2. | Toggle_automation of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. kind : [ `auto_intros | `auto_solve_trivial ];
    3. change : [ `on | `off | `toggle ];
    }
  3. | Type of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. scrutinee : Synprs__.Synprs_definition.Comp.Expression_object.t;
    }
  4. | Info of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. kind : [ `prog ];
    3. object_identifier : Beluga_syntax.Syncom.Qualified_identifier.t;
    }
  5. | Select_theorem of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. theorem : Beluga_syntax.Syncom.Qualified_identifier.t;
    }
  6. | Theorem of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. subcommand : [ `list | `defer | `show_ihs | `show_proof | `dump_proof of Support.String.t ];
    }
  7. | Session of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. subcommand : [ `list | `defer | `create | `serialize ];
    }
  8. | Subgoal of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. subcommand : [ `list | `defer ];
    }
  9. | Undo of {
    1. location : Beluga_syntax.Syncom.Location.t;
    }
  10. | Redo of {
    1. location : Beluga_syntax.Syncom.Location.t;
    }
  11. | History of {
    1. location : Beluga_syntax.Syncom.Location.t;
    }
  12. | Translate of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. theorem : Beluga_syntax.Syncom.Qualified_identifier.t;
    }
  13. | Intros of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. introduced_variables : Beluga_syntax.Syncom.Identifier.t Support.List1.t Support.Option.t;
    }
  14. | Split of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. scrutinee : Synprs__.Synprs_definition.Comp.Expression_object.t;
    }
  15. | Invert of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. scrutinee : Synprs__.Synprs_definition.Comp.Expression_object.t;
    }
  16. | Impossible of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. scrutinee : Synprs__.Synprs_definition.Comp.Expression_object.t;
    }
  17. | Msplit of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t * [ `Plain | `Hash | `Dollar ];
    }
  18. | Solve of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. solution : Synprs__.Synprs_definition.Comp.Expression_object.t;
    }
  19. | Unbox of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. expression : Synprs__.Synprs_definition.Comp.Expression_object.t;
    3. assignee : Beluga_syntax.Syncom.Identifier.t * [ `Plain | `Hash | `Dollar ];
    4. modifier : [ `Strengthened ] Support.Option.t;
    }
  20. | By of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. expression : Synprs__.Synprs_definition.Comp.Expression_object.t;
    3. assignee : Beluga_syntax.Syncom.Identifier.t;
    }
  21. | Suffices of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. implication : Synprs__.Synprs_definition.Comp.Expression_object.t;
    3. goal_premises : [ `exact of Synprs__.Synprs_definition.Comp.Sort_object.t | `infer of Beluga_syntax.Syncom.Location.t ] Support.List.t;
    }
  22. | Help of {
    1. location : Beluga_syntax.Syncom.Location.t;
    }
  23. | Auto_invert_solve of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. max_depth : Support.Int.t Support.Option.t;
    }
  24. | Inductive_auto_solve of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. max_depth : Support.Int.t Support.Option.t;
    }