diff options
Diffstat (limited to 'src/Inky/Binding.idr')
| -rw-r--r-- | src/Inky/Binding.idr | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/Inky/Binding.idr b/src/Inky/Binding.idr index 7562f27..4d8260a 100644 --- a/src/Inky/Binding.idr +++ b/src/Inky/Binding.idr @@ -71,16 +71,16 @@ BS = S -- Binders to names ------------------------------------------------------------ export -name : forall w. (b : Binder) -> Name (w :< b) -name b = Element b ((snocSem w b b).rightToLeft (Left Refl)) +nameOf : forall w. (b : Binder) -> Name (w :< b) +nameOf b = Element b ((snocSem w b b).rightToLeft (Left Refl)) export binder : Name w -> Binder binder = fst export -binderName : binder {w = w :< b} (name {w} b) = b -binderName = Refl +binderNameOf : binder {w = w :< b} (nameOf {w} b) = b +binderNameOf = Refl -- Empty world ----------------------------------------------------------------- @@ -115,6 +115,10 @@ strip (Element n member) = id $ (snocSem w b n).leftToRight member)) +public export +stripWith : {b : Binder} -> Lazy a -> Lazy (Name w -> a) -> Name (w :< b) -> a +stripWith x f = maybe x f . strip + -- Freshness ------------------------------------------------------------------- export @@ -135,7 +139,7 @@ soRecomputable : (0 s : So b) -> So b soRecomputable Oh = Oh export -sucFresh : b `FreshIn` w -> S b `FreshIn` w :< b +sucFresh : b `FreshIn` w -> BS b `FreshIn` w :< b sucFresh prf = soRecomputable (snocLength w b prf) -- World inclusion ------------------------------------------------------------- |