Merge pull request #8 from stefan-hoeck/hconst

[ new ] added hconst utility
stefan-hoeck · Nov 15, 2023 · 0290a07 · 0290a07
2 parents be1a8c0 + 4440d7a
commit 0290a07
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/Data/List/Quantifiers/Extra.idr b/src/Data/List/Quantifiers/Extra.idr
@@ -127,6 +127,10 @@ namespace All
   hfill {ks = []}    g = []
   hfill {ks = v::vs} g = g v :: hfill g
 
+  public export %inline
+  hconst : {ks : _} -> t -> All (Prelude.const t) ks
+  hconst = hfill . const
+
   public export
   hpure : All (Prelude.const ()) ks => ({0 v : k} -> f v) -> All f ks
   hpure @{[]}     fun = []