val rewrite_tac:
direction:[`LeftToRight | `RightToLeft] ->
- pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
+
val rewrite_simpl_tac:
direction:[`LeftToRight | `RightToLeft] ->
- pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic
val replace_tac:
- pattern:ProofEngineTypes.pattern ->
- with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
+ pattern:ProofEngineTypes.lazy_pattern ->
+ with_what:Cic.lazy_term -> ProofEngineTypes.tactic
val reflexivity_tac: ProofEngineTypes.tactic
val symmetry_tac: ProofEngineTypes.tactic