liamoc.net / holbert-ng
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.

fix merge issue

Liam O’Connor 675c7b28 153e6a5b

+1 -1
+1 -1
src/Method.res
··· 662 662 663 663 ctx.facts->Dict.forEachWithKey((eqRule, name) => { 664 664 if isEqualityRule(eqRule) { 665 - let insts = eqRule->Rule.schematise(gen, ~scope=ctx.fixes) 665 + let insts = eqRule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes) 666 666 let instantiatedRule = eqRule->Rule.instantiate(insts) 667 667 668 668 switch extractEqualityTermsFromBare(instantiatedRule) {