def drop
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as Fieldimport Base
65def drop(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
66 match n:
67 case 0n:
68 xs
69 case 1n+m:
70 match xs:
71 case Nil{}:
72 Nil{}
73 case Con{x, xt}:
74 drop(m, xt)
Uses (3)
Used by (13)
- bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field:wide
- bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519:verify_raw
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly:drop_lea
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes:drop_eq
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw:wide_mod
- …