diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-17 17:37:11 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-17 17:37:11 +0000 |
| commit | a8d4301d0d6e62b75abecb8e00e26e14c890a42d (patch) | |
| tree | 462b383e3d5d5057fe6e67d568ba8479f13ebf51 | |
| parent | e42f16505814d2995f771581424b2ebbfb402a49 (diff) | |
Make fullBounds public.
| -rw-r--r-- | src/Obs/Term.idr | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr index cb9701de..3e2d4b7 100644 --- a/src/Obs/Term.idr +++ b/src/Obs/Term.idr @@ -29,6 +29,7 @@ data Block : Nat -> Type where -- Operations ------------------------------------------------------------------ +export fullBounds : Term n -> Bounds fullBounds (Var x i) = x fullBounds (Sort x s) = x |