1 files changed, 6 insertions, 0 deletions
diff --git a/cheri/sail_latexcc/sailccfngetCapLength.tex b/cheri/sail_latexcc/sailccfngetCapLength.tex
new file mode 100644
index 00000000..e9ce6566
--- /dev/null
+++ b/cheri/sail_latexcc/sailccfngetCapLength.tex
@@ -0,0 +1,6 @@
+function #\hyperref[zgetCapLength]{getCapLength}#(c) : CapStruct -> CapLen =
+         let 'top = #\hyperref[zgetCapTop]{getCapTop}#(c) in
+         let 'base = #\hyperref[zgetCapBase]{getCapBase}#(c) in {
+             assert (top >= base);
+             top - base
+         }