ProofAutomationTactics

📁 Source: MRiscX/Tactics/ProofAutomationTactics.lean

Statistics

Metric	Count
Definitions alts', parse, tacticApply_spec_, tacticApply_spec_basic_, tacticApply_spec_default_, tacticApply_spec_for_second_, tacticApply_spec_when_ready_, tacticAutoSeq, tacticHoare_simp_specification, tacticPrepare_second_seq, tacticSimp_currInstr, tacticSimp_jump_spec, tacticSimp_jump_spec_false, tacticSimp_jump_spec_true, tacticSimp_t_update, tacticSplit_condisIn_, tacticZero_lt_ne_zero, «tacticSapply_s_seq'''P:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_», «tacticSapply_s_seq'''R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_», «tacticSapply_s_seq''P:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_», «tacticSapply_s_seq''R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_», «tacticSapply_s_seq''_,_,_,_,_», «tacticSapply_s_seq'_,_,_,_», «tacticSapply_s_seq_,_,_,_», «tacticSapply_s_seq_plainP:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_», «tacticSapply_s_seq_plainR:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_»	26
Theorems	0
Total	26

RCasesPatt

Definitions

Name	Category	Theorems
alts' 📖	CompOp	—
parse 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
tacticApply_spec_ 📖	CompOp	—
tacticApply_spec_basic_ 📖	CompOp	—
tacticApply_spec_default_ 📖	CompOp	—
tacticApply_spec_for_second_ 📖	CompOp	—
tacticApply_spec_when_ready_ 📖	CompOp	—
tacticAutoSeq 📖	CompOp	—
tacticHoare_simp_specification 📖	CompOp	—
tacticPrepare_second_seq 📖	CompOp	—
tacticSimp_currInstr 📖	CompOp	—
tacticSimp_jump_spec 📖	CompOp	—
tacticSimp_jump_spec_false 📖	CompOp	—
tacticSimp_jump_spec_true 📖	CompOp	—
tacticSimp_t_update 📖	CompOp	—
tacticSplit_condisIn_ 📖	CompOp	—
tacticZero_lt_ne_zero 📖	CompOp	—
«tacticSapply_s_seq'''P:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» 📖	CompOp	—
«tacticSapply_s_seq'''R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» 📖	CompOp	—
«tacticSapply_s_seq''P:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» 📖	CompOp	—
«tacticSapply_s_seq''R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» 📖	CompOp	—
«tacticSapply_s_seq''_,_,_,_,_» 📖	CompOp	—
«tacticSapply_s_seq'_,_,_,_» 📖	CompOp	—
«tacticSapply_s_seq_,_,_,_» 📖	CompOp	—
«tacticSapply_s_seq_plainP:=_,R:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» 📖	CompOp	—
«tacticSapply_s_seq_plainR:=_,L_W:=_,L_W':=_,L_B:=_,L_B':=_» 📖	CompOp	—

---

← Back to Index