Speed and optimization are becoming more and more crucial as the transpiler seems to be working decently now. Now we can start to implement analysis/pass stages into the transpiler, beginning with simple rewriting rules. Here we implement just one rule: OfNat.ofNat Nat n (instOfNatNat n) => n.
Note: This is being done as a standalone PR because adding this will just barely optimize enough to make the yatima prove .. command run in an acceptable amount of time (<1 min).
Speed and optimization are becoming more and more crucial as the transpiler seems to be working decently now. Now we can start to implement analysis/pass stages into the transpiler, beginning with simple rewriting rules. Here we implement just one rule:
OfNat.ofNat Nat n (instOfNatNat n) => n.Note: This is being done as a standalone PR because adding this will just barely optimize enough to make the
yatima prove ..command run in an acceptable amount of time (<1 min).