Skip to content

Commit 3b067c9

Browse files
committed
feat: Add trivial Padding.get
1 parent 8dad035 commit 3b067c9

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

KLR/Util/Padding.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,8 @@ deriving Inhabited
2727

2828
namespace Padding
2929

30+
def get (_ : Padding n) (_ : Nat) : Nat := 0
31+
3032
instance : GetElem (Padding n) Nat Nat (fun _ i => i < n) where
3133
getElem _ _ _ := 0
3234

0 commit comments

Comments
 (0)