Proof checking at higher abstraction level
Compare changes
- Sankalp Gambhir authored
@@ -12,13 +12,37 @@ import lisa.utils.tactics.ProofStepLib.{_, given}
@@ -29,30 +53,54 @@ object BasicStepTactic {
@@ -76,33 +124,57 @@ object BasicStepTactic {
@@ -125,31 +197,50 @@ object BasicStepTactic {
@@ -164,28 +255,49 @@ object BasicStepTactic {
@@ -207,21 +319,50 @@ object BasicStepTactic {
@@ -229,7 +370,7 @@ object BasicStepTactic {
@@ -244,21 +385,44 @@ object BasicStepTactic {
@@ -266,7 +430,7 @@ object BasicStepTactic {
@@ -282,25 +446,48 @@ object BasicStepTactic {
@@ -313,10 +500,10 @@ object BasicStepTactic {
@@ -343,18 +530,43 @@ object BasicStepTactic {
@@ -365,24 +577,24 @@ object BasicStepTactic {
@@ -397,41 +609,66 @@ object BasicStepTactic {
@@ -446,25 +683,45 @@ object BasicStepTactic {
@@ -486,40 +743,64 @@ object BasicStepTactic {
@@ -534,30 +815,53 @@ object BasicStepTactic {
@@ -572,34 +876,57 @@ object BasicStepTactic {
@@ -608,27 +935,50 @@ object BasicStepTactic {
@@ -636,7 +986,7 @@ object BasicStepTactic {
@@ -651,18 +1001,43 @@ object BasicStepTactic {
@@ -673,24 +1048,24 @@ object BasicStepTactic {
@@ -703,32 +1078,51 @@ object BasicStepTactic {
@@ -741,14 +1135,10 @@ object BasicStepTactic {
@@ -774,41 +1164,66 @@ object BasicStepTactic {
@@ -824,8 +1239,23 @@ object BasicStepTactic {
@@ -836,20 +1266,56 @@ object BasicStepTactic {
@@ -863,20 +1329,61 @@ object BasicStepTactic {
@@ -891,8 +1398,30 @@ object BasicStepTactic {
@@ -903,8 +1432,30 @@ object BasicStepTactic {
@@ -915,8 +1466,30 @@ object BasicStepTactic {
@@ -927,8 +1500,30 @@ object BasicStepTactic {
@@ -939,8 +1534,23 @@ object BasicStepTactic {
@@ -951,16 +1561,43 @@ object BasicStepTactic {