defn: regularity tactic #150
Conversation
src/1Lab/Reflection/HLevel.agda
Outdated
| then backtrack "No possible instances, but have other decompositions to try" | ||
| else pure (tt , false) | ||
| [] → backtrack "No possible instances, but have other decompositions to try" | ||
| -- if has-alts |
There was a problem hiding this comment.
We should probably get rid of this commented out code
There was a problem hiding this comment.
Oh good shout, I forgot this was here, it's from a WIP that ended up not panning out. I'll revert the change so you can still use hlevel! to fill out a skeleton
| @@ -606,6 +608,13 @@ prop-ext! {aprop = aprop} {bprop = bprop} = prop-ext aprop bprop | |||
| → x ≡ y | |||
| Σ-prop-path! {bxprop = bxprop} = Σ-prop-path bxprop | |||
|
|
|||
| prop! | |||
There was a problem hiding this comment.
Nice, I've been wanting this one for a while!
| -- This match might make you wonder: Can't Al be a line of | ||
| -- functions, so that the transport will have more arguments? No: | ||
| -- The term is in normal form. | ||
| (do |
There was a problem hiding this comment.
Maybe we could define something like Haskell's handle and use it here? It's a bit hard to see the <|> at first glance.
There was a problem hiding this comment.
See "fold syntax" here: #152. There's a couple more places where big <|> trees could become a list.
| refl-transport _ tm′ = pure tm′ | ||
|
|
||
| -- Boring term traversal. | ||
| go pre n (var x args) = var x <$> go* pre n args |
There was a problem hiding this comment.
Is it feasible to fuse the weakening and the term traversal into a single pass here?
There was a problem hiding this comment.
Feasible yes, but I'm not sure whether it's a good idea: de Bruijn indices always own me so keeping the owning to a centralise location sounds better. It might be feasible to have helpers for like, bottom-up and top-down traversal of terms, but because of the fast Regularity-precision this traversal is kinda neither
if you don't have a definitional equality, a tactic will do, too
plt-amy
force-pushed
the
aliao/regularity
branch
from
41228ae
to
b34a720
Compare
|
@TOTBWF am I good to merge this? |
if you don't have a definitional equality, a tactic will do, too