The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword by.
apply_spec
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
apply_spec_basic
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
apply_spec_default
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
apply_spec_for_second
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
apply_spec_when_ready
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
apply_to_last_goal
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.GeneralCustomTactics
hoare_simp_specification
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
prepare_second_seq
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
sapply_s_seq
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
sapply_s_seq'
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
sapply_s_seq''
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
sapply_s_seq''
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
sapply_s_seq''
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
sapply_s_seq'''
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
sapply_s_seq'''
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
sapply_s_seq_plain
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
sapply_s_seq_plain
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
simp_currInstr
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
simp_jump_spec
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
simp_jump_spec_false
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
simp_jump_spec_true
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
simp_set_eq
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.GeneralCustomTactics
simp_t_update
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
split_condis
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics
zero_lt_ne_zero
This tactic has no documentation.
- Tags:
- Defined in module:
- MRiscX.Tactics.ProofAutomationTactics