Skip to content

Instantly share code, notes, and snippets.

View OneDist.agda
open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Product
open ≡-Reasoning
variable
A : Set
B : Set
View mfix.hs
{-# LANGUAGE RecursiveDo #-}
f = do rec a <- do a <- b
putStrLn "Hello"
return a
b <- do return $ return a :: IO (IO ())
return a
f' = do rec b <- do return $ return a :: IO (IO ())
a <- do a <- b
View local_f_indeed_is_a_function.hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Strict #-}
import Debug.Trace
h :: forall a. a -> ()
h a =
let f :: Show a => ()
f = trace "Hi" $ traceShow a ()
in ()