Any thoughts on how to find a natural number that's not in a list?

For example, input is [0, 3, 4, 1]; output should be any of 2, 5, 6, etc.

It seems like you ought to be able to do something like ∧.ℕ¬(∈?)∧ (though that's pretty clumsy), but it just fails.

Aha! Looks like ≡ⁿℕ works.

Feature request: a builtin predicate for "get the first n elements of a list," where n is given as a subscript. The closest I can think of is a₀l₃ (with *n*=3 in this case)--and that construct gets more complicated if you want to use a subscript of ₍ or ₎.

It might be possible to accomplish this with a subscript on h (and similarly for t with the last n elements), except I'm not sure how that would work with the non-subscripted case, which outputs an element, not a list containing a single element. Is it possible for [1,2,3]h to output 1 while [1,2,3]h₁ outputs [1] (and [1,2,3]h₀ outputs [] for completeness)?

@DLosc That's actually pretty cool

@DLosc Yes it's possible, because h₁ can be coded as a different case from h.

Actually, it was always planned to implement this subscript behavior with h and t, but I never implemented it

I'm gonna have a look at it

@DLosc This is now implemented as of this commit. As you can see, I removed a TODO comment about that very feature, which dates back to the first commit of Brachylog v2 on January 22, 2017. Better late than never :p

(Note that this is implemented both for h and t)

Example usage

you're welcome

@Fatalize Awesome! \o/