<commit_before>I am a File
===========

\begin{comment}
\begin{code}
module Goo where
\end{code}
\end{comment}

This is Section 1
-----------------

Yabba dabba doo now.

\begin{code}
{-@ incr :: Nat -> Nat @-}
incr :: Int -> Int
incr x = x + 1
\end{code}

And now, Section 2
------------------

Gibbity dibbity doo now.

\begin{code}
{-@ wincr :: Nat -> Nat @-}
wincr :: Int -> Int
wincr x = x - 1
\end{code}

subtyping
---------

this is the end<commit_msg>ok, the comment-code thing works for ONE file<commit_after>I am a File
===========

\begin{comment}
\begin{code}
{-@ LIQUID "--short-names" @-}
module Logic where
main :: IO ()
main = return ()


{-@ type TRUE  = {v:Bool | Prop v} @-}
{-@ type FALSE = {v:Bool | not (Prop v)} @-}


{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | Prop v <=> (Prop p =>  Prop q)} @-}
(==>) :: Bool -> Bool -> Bool
(==>) = undefined

{-@ measure f :: Int -> Int @-}
{-@ f :: x:Int -> {v:Int | v = f x} @-}
f :: Int -> Int
f = undefined
\end{code}
\end{comment}




This is Section 1
-----------------

Yabba dabba doo now.

\begin{code}
{-@ incr :: Nat -> Nat @-}
incr :: Int -> Int
incr x = x + 1
\end{code}

And now, Section 2
------------------

Gibbity dibbity doo now.

\begin{code}
{-@ wincr :: Nat -> Nat @-}
wincr :: Int -> Int
wincr x = x - 1
\end{code}

subtyping
---------

this is the end


\begin{code}
{-@ congruence :: Int -> Int -> TRUE @-}
congruence x y = (x == y) ==> (f x == f y)
\end{code}

{'fraction_non_alphanumeric': 0.2669432918395574, 'fraction_numerical': 0.005532503457814661, 'mean_word_length': 2.18021978021978, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 26, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7016204', 'n_tokens_mistral': 604, 'n_tokens_neox': 577, 'n_words': 178}