Rewriting system.

sireum · Feb 9, 2024 · 5101fb3 · 5101fb3
1 parent 139aac9
commit 5101fb3
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/library/shared/src/main/scala/org/sireum/contract.scala b/library/shared/src/main/scala/org/sireum/contract.scala
@@ -1670,6 +1670,7 @@ trait contract {
 
   implicit def $toB(state: Contract.StateCont): B = ???
 
+  implicit def $toSequent(b: Boolean): Contract.SequentBuilder = ???
   implicit def $toSequent(bs: (B, B)): Contract.SequentBuilder = ???
   implicit def $toSequent(bs: (B, B, B)): Contract.SequentBuilder = ???
   implicit def $toSequent(bs: (B, B, B, B)): Contract.SequentBuilder = ???

diff --git a/library/shared/src/main/scala/org/sireum/justification.scala b/library/shared/src/main/scala/org/sireum/justification.scala
@@ -55,7 +55,7 @@ object justification {
 
   @just def Admit: Unit = $
 
-  @just def Rewrite(rs: RS): Unit = $
+  @just def Rewrite(rs: RS, from: StepId): Unit = $
 
   object natded {