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.

reduce

澪 74b605f3 04d07746

+1 -1
+1 -1
src/HOTerm.res
··· 237 237 | App({func, arg}) => 238 238 switch reduce(func) { 239 239 | Lam({body}) => reduce(downshift(substitute(body, singletonSubst(0, upshift(arg, 1))), 1)) 240 - | _ => term 240 + | func => App({func, arg}) 241 241 } 242 242 | term => term 243 243 }