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.

add upshift to symbol signature

+8 -1
+1
src/SExp.res
··· 20 20 let ghost = "" 21 21 let substDeBruijn = (name, _, ~from as _) => name 22 22 let unifiesWithAnything = _ => false 23 + let upshift = (t, _, ~from as _=?) => t 23 24 } 24 25 25 26 include SExpFunc.Make(ConstSymbol)
+2 -1
src/SExpFunc.res
··· 5 5 let prettyPrint: (t, ~scope: array<string>) => string 6 6 let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string> 7 7 let substitute: (t, subst) => t 8 + let upshift: (t, int, ~from: int=?) => t 8 9 // used for when trying to substitute a variable of the wrong type 9 10 let lowerVar: int => t 10 11 let lowerSchematic: (int, array<int>) => t ··· 194 195 } 195 196 let rec upshift = (term: t, amount: int, ~from: int=0) => 196 197 switch term { 197 - | Symbol(_) => term 198 + | Symbol(s) => Symbol(s->Symbol.upshift(amount, ~from)) 198 199 | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => upshift(x, amount, ~from))}) 199 200 | Var({idx}) => 200 201 Var({
+5
src/StringSExp.res
··· 37 37 } 38 38 | ConstS(s) => ConstS(s) 39 39 } 40 + let upshift = (s, amount: int, ~from=?) => 41 + switch s { 42 + | StringS(s) => StringS(s->StringTerm.upshift(amount, ~from?)) 43 + | ConstS(s) => ConstS(s) 44 + } 40 45 let lowerVar = idx => StringS([StringTerm.Var({idx: idx})]) 41 46 let lowerSchematic = (schematic, allowed) => StringS([StringTerm.Schematic({schematic, allowed})]) 42 47 let ghost = StringS([StringTerm.Ghost])