JAR: Join-Accumulate Refine

4.4. Gas Allocations🔗

🔗def
Jar.G_A [j : Jar.JarConfig] : Nat
Jar.G_A [j : Jar.JarConfig] : Nat

G_A via JarConfig.

🔗def
Jar.G_I [j : Jar.JarConfig] : Nat
Jar.G_I [j : Jar.JarConfig] : Nat

G_I via JarConfig.

🔗def
Jar.G_R [j : Jar.JarConfig] : Nat
Jar.G_R [j : Jar.JarConfig] : Nat

G_R via JarConfig.

🔗def
Jar.G_T [j : Jar.JarConfig] : Nat
Jar.G_T [j : Jar.JarConfig] : Nat

G_T via JarConfig.