Created
October 26, 2016 19:56
-
-
Save jg/55eda08ed86763ed2bcf376caa3c3e9f to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
let rec eval1 ctx t = match t with | |
TmApp(fi,TmAbs(_,x,t12),v2) when isval ctx v2 -> | |
termSubstTop v2 t12 | |
| TmApp(fi,v1,t2) when isval ctx v1 -> | |
let t2' = eval1 ctx t2 in | |
TmApp(fi, v1, t2') | |
| TmApp(fi,t1,t2) -> | |
let t1' = eval1 ctx t1 in | |
TmApp(fi, t1', t2) | |
| _ -> | |
raise NoRuleApplies |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment