the next generation of the in-browser educational proof assistant
minor tweaks and fixes
+7
-3
+3
-1
src/Proof.res
+3
-1
src/Proof.res
···
48
48
~subprinter=prettyPrint,
49
49
)
50
50
}
51
+
let displayFixes = [...prf.fixes]
52
+
Array.reverse(displayFixes)
51
53
String.padStart("", indentation, " ")
52
-
->String.concat(prf.fixes->Array.map(Term.prettyPrintMeta)->Array.join(""))
54
+
->String.concat(displayFixes->Array.map(Term.prettyPrintMeta)->Array.join(""))
53
55
->String.concat(
54
56
prf.assumptions
55
57
->Array.map(s => String.concat(" ", s))
+1
-1
src/SExp.res
+1
-1
src/SExp.res
···
182
182
}
183
183
let prettyPrintVar = (idx: int, scope: array<string>) =>
184
184
switch scope[idx] {
185
-
| Some(n) if Array.indexOf(scope, n) == idx && false => n
185
+
| Some(n) if Array.indexOf(scope, n) == idx => n
186
186
| _ => "\\"->String.concat(String.make(idx))
187
187
}
188
188
let makeGen = () => {
+3
-1
src/Theorem.res
+3
-1
src/Theorem.res
···
22
22
}
23
23
let serialise = (state: state) => {
24
24
state.rule
25
-
->Rule.prettyPrintTopLevel(~name=state.name)
25
+
->Rule.prettyPrintTopLevel(~name=state.name)->String.concat("\n\n")
26
26
->String.concat(Proof.prettyPrint(state.proof, ~scope=[]))
27
27
}
28
28
let deserialise = (str: string, ~imports: Ports.t) => {
···
53
53
~exports={Ports.facts: Dict.fromArray([(props.content.name,props.content.rule)]), ruleStyle: None})
54
54
}
55
55
<>
56
+
<h3>{React.string("Theorem")}</h3>
56
57
<RuleView rule={props.content.rule} scope={[]} style={ruleStyle}>
57
58
{React.string(props.content.name)}
58
59
</RuleView>
60
+
<h4>{React.string("Proof")}</h4>
59
61
<ProofView ruleStyle={ruleStyle} scope={[]} proof=checked gen={props.content.gen} onChange=proofChanged/>
60
62
</>
61
63
}