extend set of axioms annotated with axioms dependencies
Set of symbols to annotate:
-
int.Exponentiation.power -
int.NumOf.numof -
int.Sum.sum -
int.Fact.fact -
int.Iter.iter -
int.Fibonacci.fib -
int.WFltof.ltof -
bv.Pow2.pow2 -
bv.BVgen.nth_bv -
bv.BVgen.uge -
bv.BVgen.ugt -
bv.BVgen.ule -
bv.BVgen.ult -
bv.BVgen.sge -
bv.BVgen.sgt -
bv.BVgen.sle -
bv.BVgen.slt -
option.Option.is_none -
option.Map.map -
to be continued, say with list.mlw
, etc.