the next generation of the in-browser educational proof assistant
1
fork

Configure Feed

Select the types of activity you want to include in your feed.

call seen

9f7b073a e0da9fa7

+11 -6
+11 -6
src/HOTerm.res
··· 483 483 } 484 484 | VarS({idx}) => Var({idx: idx}) 485 485 | SchematicS({schematic}) => 486 - Schematic({ 487 - schematic, 488 - allowed: env 489 - ->Map.values 490 - ->Core__Iterator.toArray, 491 - }) 486 + switch gen { 487 + | Some(g) => { 488 + seen(g, schematic) 489 + let allowed = 490 + env 491 + ->Map.values 492 + ->Core__Iterator.toArray 493 + Schematic({schematic, allowed}) 494 + } 495 + | None => raise(ParseError("Schematics not allowed here")) 496 + } 492 497 | LambdaS({name, body}) => 493 498 Lam({ 494 499 name,