A utility library to display inline pop-ups.  Looks roughly like this:


let _ = <|>le m n                           â† <|> marks the point
------------------------------------------- â† Pop-up begins here
        le : â„• â†’ â„• â†’ â„™
        Inductive le (n : â„•) : â„• â†’ â„™ â‰œ
        | le_n : n â‰¤ n
        | le_S : âˆ€ m : â„•, n â‰¤ m â†’ n â‰¤ S m
------------------------------------------- â† Pop-up ends here
        && le n m                           â† Buffer text continues here

See `quick-peek-show' and `quick-peek-hide' for usage instructions.