{"header":{"message":"rewrite following chapman thesis ch2","description":null,"timestamp":"2021-10-21T07:29:04.910563926Z","authors":[{}]},"hash":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC","authors":[{"key":"Fi16Ka6f4bget8foxQRWszq749Zub3y9dC3XmFoMpoqr"}],"deps":{"hashes":[["ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC","rewrite following chapman thesis ch2"],["AA",null],["CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC","init repo"],["QZCAUX2IKG324UC3PODLXOLS3KWVXP4JW4WP4YYSBPLXJRL2EZ3AC","init repo"]],"deps":["CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC"],"known":[]},"hunks":[{"Edit":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":4,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":999},"to":{"change":2,"start":999,"end":1054},"introduced_by":2}],"inode":{"change":2,"pos":951}}},"contents":[{"Del":{"text":"import Data.Map (Map)","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1020"}},{"Del":{"text":"import qualified Data.Map as Map","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1053"}}]}},{"Replacement":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":11,"ins":{"up_context":[{"change":2,"pos":1144}],"down_context":[{"change":2,"pos":1189}],"flag":"BLOCK","start":0,"end":89,"inode":{"change":2,"pos":951}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1144},"to":{"change":2,"start":1144,"end":1189},"introduced_by":2}],"inode":{"change":2,"pos":951}},"ins_contents":[{"Add":{"text":"data Term","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:9"}},{"Add":{"text":" = Var Index","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:23"}},{"Add":{"text":" | Pi Term Term","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:40"}},{"Add":{"text":" | Lam Term","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:53"}},{"Add":{"text":" | Term :$ Term","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:70"}},{"Add":{"text":" | Ann Term Term","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:88"}}],"del_contents":[{"Del":{"text":"data TermInf","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1156"}},{"Del":{"text":" = Global Name","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1172"}},{"Del":{"text":" | Local Index","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1188"}}]}},{"Edit":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":18,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1198},"to":{"change":2,"start":1198,"end":1291},"introduced_by":2}],"inode":{"change":2,"pos":951}}},"contents":[{"Del":{"text":" | Ann TermChk TermChk","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1221"}},{"Del":{"text":" | App TermChk TermInf","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1245"}},{"Del":{"text":" | Pi TermChk TermChk","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1268"}},{"Del":{"text":" deriving (Eq, Show)","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1290"}}]}},{"Replacement":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":19,"ins":{"up_context":[{"change":2,"pos":1292}],"down_context":[{"change":2,"pos":1359}],"flag":"BLOCK","start":90,"end":158,"inode":{"change":2,"pos":951}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1292},"to":{"change":2,"start":1292,"end":1359},"introduced_by":2}],"inode":{"change":2,"pos":951}},"ins_contents":[{"Add":{"text":"data Val","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:98"}},{"Add":{"text":" = VLam Term Env","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:116"}},{"Add":{"text":" | VPi Val Term Env","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:137"}},{"Add":{"text":" | VStar","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:147"}},{"Add":{"text":" | Ne Ne","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:157"}}],"del_contents":[{"Del":{"text":"data TermChk","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1304"}},{"Del":{"text":" = Inf TermInf","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1320"}},{"Del":{"text":" | Lam TermChk","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1336"}},{"Del":{"text":" deriving (Eq, Show)","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1358"}}]}},{"Replacement":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":25,"ins":{"up_context":[{"change":2,"pos":1360}],"down_context":[{"change":2,"pos":1444}],"flag":"BLOCK","start":159,"end":191,"inode":{"change":2,"pos":951}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1360},"to":{"change":2,"start":1360,"end":1444},"introduced_by":2}],"inode":{"change":2,"pos":951}},"ins_contents":[{"Add":{"text":"data Ne = NV Index | Ne :$$ Val","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:190"}}],"del_contents":[{"Del":{"text":"data Value","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1370"}},{"Del":{"text":" = VStar","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1380"}},{"Del":{"text":" | VLam TermChk","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1397"}},{"Del":{"text":" | VPi TermChk TermChk","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1421"}},{"Del":{"text":" deriving (Eq, Show)","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1443"}}]}},{"Replacement":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":27,"ins":{"up_context":[{"change":2,"pos":1445}],"down_context":[{"change":2,"pos":1471}],"flag":"BLOCK","start":192,"end":209,"inode":{"change":2,"pos":951}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1445},"to":{"change":2,"start":1445,"end":1471},"introduced_by":2}],"inode":{"change":2,"pos":951}},"ins_contents":[{"Add":{"text":"type Env = [Val]","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:208"}}],"del_contents":[{"Del":{"text":"type Env = Map Name Value","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1470"}}]}},{"Replacement":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":29,"ins":{"up_context":[{"change":2,"pos":1472}],"down_context":[{"change":2,"pos":1503}],"flag":"BLOCK","start":210,"end":227,"inode":{"change":2,"pos":951}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1472},"to":{"change":2,"start":1472,"end":1503},"introduced_by":2}],"inode":{"change":2,"pos":951}},"ins_contents":[{"Add":{"text":"type Ctx = [Val]","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:226"}}],"del_contents":[{"Del":{"text":"empty :: Env","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1484"}},{"Del":{"text":"empty = Map.empty","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1502"}}]}},{"Replacement":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":31,"ins":{"up_context":[{"change":2,"pos":1504}],"down_context":[{"change":2,"pos":1523}],"flag":"BLOCK","start":228,"end":521,"inode":{"change":2,"pos":951}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1504},"to":{"change":2,"start":1504,"end":1523},"introduced_by":2}],"inode":{"change":2,"pos":951}},"ins_contents":[{"Add":{"text":"whnf :: Term -> Env -> Maybe Val","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:260"}},{"Add":{"text":"whnf (Var i) env = env !! i","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:288"}},{"Add":{"text":"whnf (Pi d r) env = do","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:311"}},{"Add":{"text":" vd <- (whnf d env)","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:332"}},{"Add":{"text":" Just $ VPi vd r env","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:354"}},{"Add":{"text":"whnf (Lam t) env = Just $ VLam t env","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:391"}},{"Add":{"text":"whnf (f :$ a) env = do","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:414"}},{"Add":{"text":" vf <- whnf f env","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:433"}},{"Add":{"text":" va <- whnf a env","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:452"}},{"Add":{"text":" vf $$ va","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:463"}},{"Add":{"text":"whnf (Ann t _) env = whnf t env","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:495"}},{"Add":{"text":"whnf Star _ = Just VStar","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:520"}}],"del_contents":[{"Del":{"text":"type Ctx = [Value]","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1522"}}]}},{"Replacement":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":44,"ins":{"up_context":[{"change":2,"pos":1524}],"down_context":[{"change":2,"pos":1569}],"flag":"BLOCK","start":522,"end":640,"inode":{"change":2,"pos":951}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1524},"to":{"change":2,"start":1524,"end":1569},"introduced_by":2}],"inode":{"change":2,"pos":951}},"ins_contents":[{"Add":{"text":"($$) :: Val -> Val -> Maybe Val","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:553"}},{"Add":{"text":"(VLam r env) $$ a = whnf r (a : env)","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:590"}},{"Add":{"text":"Ne n $$ a = Just (Ne (n :$$ a))","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:622"}},{"Add":{"text":"_ $$ _ = Nothing","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:639"}}],"del_contents":[{"Del":{"text":"type Eval t = Env -> Ctx -> t -> Maybe Value","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1568"}}]}},{"Replacement":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":49,"ins":{"up_context":[{"change":2,"pos":1570}],"down_context":[{"change":2,"pos":1999}],"flag":"BLOCK","start":641,"end":841,"inode":{"change":2,"pos":951}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1570},"to":{"change":2,"start":1570,"end":1999},"introduced_by":2}],"inode":{"change":2,"pos":951}},"ins_contents":[{"Add":{"text":"wk :: Val -> Val","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:657"}},{"Add":{"text":"wk (VLam t env) = VLam t (ewk env)","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:692"}},{"Add":{"text":"wk (VPi d r env) = VPi (wk d) r (ewk env)","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:734"}},{"Add":{"text":"wk VStar = VStar","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:751"}},{"Add":{"text":"wk (Ne ne) = Ne $ nwk ne","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:776"}},{"Add":{"text":"","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:777"}},{"Add":{"text":"ewk :: Env -> Env","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:795"}},{"Add":{"text":"ewk = map wk","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:808"}},{"Add":{"text":"","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:809"}},{"Add":{"text":"cwk :: Ctx -> Ctx","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:827"}},{"Add":{"text":"cwk = map wk","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:840"}}],"del_contents":[{"Del":{"text":"evalInf :: Eval TermInf","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1593"}},{"Del":{"text":"evalInf env ctx (Global n) = Map.lookup n env","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1639"}},{"Del":{"text":"evalInf env ctx (Local idx) = ctx !! idx","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1680"}},{"Del":{"text":"evalInf env ctx Star = Just VStar","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1714"}},{"Del":{"text":"evalInf env ctx (Ann t _) = evalChk env ctx t","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1760"}},{"Del":{"text":"evalInf env ctx (App f a) = do","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1791"}},{"Del":{"text":" a <- evalInf env ctx a","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1816"}},{"Del":{"text":" case evalChk env ctx f of","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1844"}},{"Del":{"text":" Just (VLam b) -> evalChk env (a : ctx) b","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1889"}},{"Del":{"text":" Just (VPi _ b) -> evalChk env (a : ctx) b","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1935"}},{"Del":{"text":" _ -> Nothing","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1952"}},{"Del":{"text":"evalInf env ctx (Pi dom t) = Just (VPi dom t)","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:1998"}}]}},{"Replacement":{"inode":{"change":2,"pos":951},"path":"src/AST.hs","line":61,"ins":{"up_context":[{"change":2,"pos":2000}],"down_context":[],"flag":"BLOCK","start":842,"end":1689,"inode":{"change":2,"pos":951}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":2000},"to":{"change":2,"start":2000,"end":2120},"introduced_by":2}],"inode":{"change":2,"pos":951}},"ins_contents":[{"Add":{"text":"nwk :: Ne -> Ne","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:857"}},{"Add":{"text":"nwk (NV i) = NV (i + 1)","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:881"}},{"Add":{"text":"nwk (n :$$ v) = nwk n :$$ wk v","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:912"}},{"Add":{"text":"","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:913"}},{"Add":{"text":"fresh :: Val","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:926"}},{"Add":{"text":"fresh = Ne (NV 0)","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:944"}},{"Add":{"text":"","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:945"}},{"Add":{"text":"eq :: Ctx -> Val -> Val -> Val -> Maybe ()","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:988"}},{"Add":{"text":"eq _ VStar VStar VStar = return ()","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1023"}},{"Add":{"text":"eq ctx VStar (VPi d1 r1 env1) (VPi d2 r2 env2) = do","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1075"}},{"Add":{"text":" eq ctx VStar d1 d2","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1096"}},{"Add":{"text":" whnfr1 <- (whnf r1 ((Ne (NV 0)) : ewk env1))","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1143"}},{"Add":{"text":" whnfr2 <- (whnf r2 ((Ne (NV 0)) : ewk env2))","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1190"}},{"Add":{"text":" eq (fresh : cwk ctx) VStar whnfr1 whnfr2","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1233"}},{"Add":{"text":"eq ctx (VPi _ r env) f g = do","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1263"}},{"Add":{"text":" vr <- whnf r ((Ne (NV 0)) : ewk env)","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1302"}},{"Add":{"text":" vf <- wk f $$ (Ne (NV 0))","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1330"}},{"Add":{"text":" vg <- wk g $$ (Ne (NV 0))","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1358"}},{"Add":{"text":" eq (fresh : cwk ctx) vr vf vg","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1390"}},{"Add":{"text":"eq ctx _ (Ne n1) (Ne n2) = neq ctx n1 n2 >> return ()","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1444"}},{"Add":{"text":"eq _ _ _ _ = Nothing","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1465"}},{"Add":{"text":"","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1466"}},{"Add":{"text":"neq :: Ctx -> Ne -> Ne -> Maybe Val","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1502"}},{"Add":{"text":"neq ctx (NV i) (NV j) = if i == j then ctx !! i else Nothing","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1563"}},{"Add":{"text":"neq ctx (n1 :$$ v1) (n2 :$$ v2) = do","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1600"}},{"Add":{"text":" VPi d r env <- neq ctx n1 n2","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1631"}},{"Add":{"text":" eq ctx d v1 v2","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1648"}},{"Add":{"text":" whnf r (v1 : env)","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1668"}},{"Add":{"text":"neq _ _ _ = Nothing","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1688"}}],"del_contents":[{"Del":{"text":"evalChk :: Eval TermChk","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:2023"}},{"Del":{"text":"evalChk env ctx (Inf term) = evalInf env ctx term","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:2073"}},{"Del":{"text":"evalChk env ctx (Lam body) = Just (VLam body)","pos":"CNWLL7RY3PNQBCWOAHFVSRHVHK3YZUN2QW5KZAW7WN5IZVYUMJAQC:2119"}}]}},{"Edit":{"inode":{"change":4,"pos":926},"path":"CoreTT.cabal","line":34,"atom":{"NewVertex":{"up_context":[{"change":4,"pos":1710}],"down_context":[{"change":4,"pos":1710}],"flag":"BLOCK","start":1690,"end":1776,"inode":{"change":4,"pos":926}}},"contents":[{"Add":{"text":" ghc-options:","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1706"}},{"Add":{"text":" -Wall","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1720"}},{"Add":{"text":" -Werror","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1736"}},{"Add":{"text":" -fwarn-incomplete-uni-patterns","pos":"ZDIH6EDAYCMZIQHUEMQVWN4L3UBBY7SHARY6DYQMBZTSTDA4MHXAC:1775"}}]}}],"owner":"n-osborne","repo":"CoreTT","token":"2WdqhAnNL2YYBQNQeLWoP62AWZgQdjze20Wk+oQBkVY=","login":null}

…

Dependencies

Change contents

Review