the next generation of the in-browser educational proof assistant
check for distinct bound variable
+6
-1
+6
-1
src/HOTerm.res
+6
-1
src/HOTerm.res
···
343
343
| _ => None
344
344
}
345
345
)
346
-
if gen->Option.isNone || map->Array.find(v => v->Option.isNone)->Option.isSome {
346
+
let set = Belt.Set.fromArray(map->Array.keepSome, ~id=module(IntCmp))
347
+
if (
348
+
gen->Option.isNone ||
349
+
map->Array.find(v => v->Option.isNone)->Option.isSome ||
350
+
set->Belt.Set.size < allowed->Array.length
351
+
) {
347
352
None
348
353
} else {
349
354
let substV: substVar = Map.make()