Activity
added more theorems in LibMisc and renamed LibStruct to LibMisc
added more theorems in LibMisc and renamed LibStruct to LibMisc
more notations for returning LetE's
more notations for returning LetE's
remove Fin from Export module list
remove Fin from Export module list
using length instead of inferred value
using length instead of inferred value
modified extraction to not generate spurious writers for method calls
modified extraction to not generate spurious writers for method calls
Changed Struct Kind's index to have a single function from Fin.t to (…
Changed Struct Kind's index to have a single function from Fin.t to (…
updated tutorial with a more complicated invariant
updated tutorial with a more complicated invariant
using the new 'Sub' notation in Kami
using the new 'Sub' notation in Kami
adding a few more theorems for word arithmetic
adding a few more theorems for word arithmetic
switched order of msb and lsb in SignExtend to match ZeroExtend
switched order of msb and lsb in SignExtend to match ZeroExtend
Fixed the associativity of if-then-else - fixed a parse error
Fixed the associativity of if-then-else - fixed a parse error
Removing RecordUpdate, fixing order of nat and string
Removing RecordUpdate, fixing order of nat and string
Upgrade Coq and Haskell Versions
Upgrade Coq and Haskell Versions
Pull request merge
Coq version 8.16.1 and GHC 9.4.4
Coq version 8.16.1 and GHC 9.4.4