gistfile1.txt

module SIMPLE-SYNTAX

endmodule

module SIMPLE
  
  imports BOOL
  imports INT

  syntax Bitfield ::= Bitfield Bit
                    | Bit

  syntax Bit ::= "l" | "h"

  syntax Int ::= "bToI" "(" Bit ")"
               | "bfToI" "(" Bitfield ")"

  rule bToI(l:Bit) => 0
  rule bToI(h:Bit) => 1

  rule bfToI(XS:Bitfield X:Bit) => (bfToI(XS) *Int 2) +Int bToI(X)
  rule bfToI(X:Bit) => bToI(X)

endmodule

--------------------

module SIMPLE-SPEC
    imports SIMPLE

    rule <k> bfToI(XS) => 5 </k>

endmodule


--------------------

# kprove simple-spec.k
[WARNING] Running as root is not recommended
kore-exec: Error in module 'SIMPLE' -> symbol 'LblbToI'LParUndsRParUnds'SIMPLE'Unds'Int'Unds'Bit' declaration (/mnt/c/Users/Bryan/Documents/kframework/frist/./.kprove-2019-10-21-13-48-25-951-d03973dc-45a9-4a26-aa2f-4433aa3cf0ad/vdefinition.kore 148:10): Cannot define constructor 'LblbToI'LParUndsRParUnds'SIMPLE'Unds'Int'Unds'Bit' for hooked sort 'SortInt{}'.
CallStack (from HasCallStack):
  error, called at app/share/GlobalMain.hs:441:36 in main:GlobalMain
[Error] Internal: Uncaught exception thrown of type FileNotFoundException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
(./.kprove-2019-10-21-13-48-25-951-d03973dc-45a9-4a26-aa2f-4433aa3cf0ad/result.kore
(No such file or directory))