Skip to content

Commit

Permalink
fixed type error
Browse files Browse the repository at this point in the history
  • Loading branch information
karthikbhargavan committed Jul 14, 2024
1 parent 1e99b0e commit adcbf6a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion proof-libs/fstar/core/Core.Num.fsti
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ val impl__u16__pow (base: u16) (exponent: u32): result : u16 {v base == 2 /\ v e
val impl__u32__pow (base: u32) (exponent: u32): result : u32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.U32 (pow2 (v exponent))}
val impl__u64__pow: u64 -> u32 -> u64
val impl__u128__pow: u128 -> u32 -> u128
val impl__i16__pow (base: i16) (exponent: u32): result: i16 {v base == 2 /\ v exponent < 16 ==> result == mk_int #Lib.IntTypes.S16 (pow2 (v exponent))}
val impl__i16__pow (base: i16) (exponent: u32): result: i16 {v base == 2 /\ v exponent < 15 ==> result == mk_int #Lib.IntTypes.S16 (pow2 (v exponent))}
val impl__i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.S32 (pow2 (v exponent))}

val impl__u8__count_ones: u8 -> u32
Expand Down

0 comments on commit adcbf6a

Please sign in to comment.