The following code exhibits several false positives and false negatives for the LFS flat sequence constructor:
namespace http://mathhub.info/Panoptikum/examples❚
theory flexary_connectives :ur:?LFS =
prop : type ❙
flexand : {n} prop^n ⟶ prop❘# ⋀ 2❙
flex_impl : {n}prop^n ⟶ prop ⟶ prop❘# 2 %R⇒_ 1 3 prec 10❙
a:prop ❙
b: prop ❙
c: prop ❙
/T Should check: ❙
f: prop^1 ❘= ⟨a⟩❙
/T Should check: ❙
d : prop^2 ❘ = ⟨a,b⟩❙
/T Should not check: ❙
e : prop^3 ❘ = ⟨a,b⟩❙
/T Should check: ❙
andtest : prop ❘= ⋀ ⟨a,b⟩❙
/T Should check: ❙
andtesttwo : prop ❘ = flexand 2 ⟨a,b⟩❙
/T Should check: ❙
works = ⟨a⟩ ⇒_ 1 b ❙
/T Should not check: ❙
test = ⟨a⟩ ⇒_ 3 b ❙
/T Should check: ❙
test_two = ⟨a,b⟩ ⇒_ 2 c ❙
/T Should not check: ❙
test_three = ⟨a,b,b⟩ ⇒_ 1 b ❙
/T Should not check: ❙
test_four = ⟨a,b,b⟩ ⇒_ 5 b ❙
/T Should check: ❙
test_five = ⟨a,b,b⟩ ⇒_ 3 b ❙
❚
In summary, automatic inference of arity fails; when explicity provided with an arity, only the case for n=1 works. False positives abound when providing wrong arities.
The following code exhibits several false positives and false negatives for the LFS flat sequence constructor:
In summary, automatic inference of arity fails; when explicity provided with an arity, only the case for n=1 works. False positives abound when providing wrong arities.