Commit 1e773887 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Tue Apr 30 01:57:08 CEST 2019)

parent 2e5ad3be
...@@ -170,16 +170,18 @@ instance (Show a,IsCapriconString str,MonadReader (Env str (Term str a)) m,Monad ...@@ -170,16 +170,18 @@ instance (Show a,IsCapriconString str,MonadReader (Env str (Term str a)) m,Monad
return (ContextTerm d' $ inc_depth (d'-d) e) return (ContextTerm d' $ inc_depth (d'-d) e)
substHyp h vh = do substHyp h vh = do
ContextTerm dm vh' <- pullTerm (Just h) vh ContextTerm dh vh' <- pullTerm (Just h) vh
dm <- length <$> ask
first (\f cv@(ContextTerm d v) -> first (\f cv@(ContextTerm d v) ->
if d < debug dm then trace "no" cv if d <= dh then cv
else trace "yes" $ ContextTerm (d-1) (f v)) <$> else ContextTerm (d-1) (inc_depth (d-dm) $ f $ inc_depth (dm-d) v)) <$>
substHyp h vh' substHyp h vh'
insertHypBefore h h' cth' = do insertHypBefore h h' cth' = do
ContextTerm dh th' <- pullTerm h cth' ContextTerm dh th' <- pullTerm h cth'
dm <- length <$> ask
first (\f cx@(ContextTerm d x) -> first (\f cx@(ContextTerm d x) ->
if d <= dh then cx if d <= dh then cx
else ContextTerm (d+1) (inc_depth (d-dh) $ f $ inc_depth (dh-d) x)) else ContextTerm (d+1) (inc_depth (d-dm) $ f $ inc_depth (dm-d) x))
<$> insertHypBefore h h' th' <$> insertHypBefore h h' th'
data NodeDir str ax a = NodeDir data NodeDir str ax a = NodeDir
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment