diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
index e5cef418af..8aa2967c74 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
@@ -46,8 +46,9 @@ makeLenses ''IndApp
 
 data Expression
   = ExprIden Name
+  | ExprUndefined
   | ExprLiteral Literal
-  | ExprApp App
+  | ExprApp Application
   | ExprLet Let
   | ExprIf If
   | ExprCase Case
@@ -57,7 +58,7 @@ data Literal
   = LitNumeric Integer
   | LitString Text
 
-data App = App
+data Application = Application
   { _appLeft :: Expression,
     _appRight :: Expression
   }
@@ -99,7 +100,7 @@ data ConstrApp = ConstrApp
     _constrAppArgs :: [Pattern]
   }
 
-makeLenses ''App
+makeLenses ''Application
 makeLenses ''Let
 makeLenses ''If
 makeLenses ''Case
@@ -117,12 +118,15 @@ data Statement
 
 data Definition = Definition
   { _definitionName :: Name,
-    _definitionType :: Type
+    _definitionType :: Type,
+    _definitionBody :: Expression
   }
 
 data Function = Function
   { _functionName :: Name,
-    _functionType :: Type
+    _functionType :: Type,
+    _functionArgs :: NonEmpty Name,
+    _functionBody :: Expression
   }
 
 data Synonym = Synonym
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
index 1924fc9a53..76e2b86cd1 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -61,6 +61,73 @@ instance PrettyCode IndApp where
     ind <- ppCode _indAppInductive
     return $ params <?+> ind
 
+instance PrettyCode Expression where
+  ppCode = \case
+    ExprIden x -> ppCode x
+    ExprUndefined -> return kwUndefined
+    ExprLiteral x -> ppCode x
+    ExprApp x -> ppCode x
+    ExprLet x -> ppCode x
+    ExprIf x -> ppCode x
+    ExprCase x -> ppCode x
+    ExprLambda x -> ppCode x
+
+instance PrettyCode Literal where
+  ppCode = \case
+    LitNumeric x -> return $ annotate AnnLiteralInteger (pretty x)
+    LitString x -> return $ annotate AnnLiteralString $ squotes $ squotes $ pretty x
+
+instance PrettyCode Application where
+  ppCode Application {..} = do
+    l <- ppCode _appLeft
+    r <- ppCode _appRight
+    return $ l <+> r
+
+instance PrettyCode Let where
+  ppCode Let {..} = do
+    name <- ppCode _letVar
+    val <- ppCode _letValue
+    body <- ppCode _letBody
+    return $ parens $ kwLet <+> name <+> "=" <+> val <+> kwIn <+> body
+
+instance PrettyCode If where
+  ppCode If {..} = do
+    val <- ppCode _ifValue
+    br1 <- ppCode _ifBranchTrue
+    br2 <- ppCode _ifBranchFalse
+    return $ parens $ kwIf <+> val <+> kwThen <+> br1 <+> kwElse <+> br2
+
+instance PrettyCode Case where
+  ppCode Case {..} = do
+    val <- ppCode _caseValue
+    brs <- toList <$> mapM ppCode _caseBranches
+    let brs' = punctuate kwPipe brs
+    return $ parens $ kwCase <+> val <+> kwOf <+> hsep brs'
+
+instance PrettyCode CaseBranch where
+  ppCode CaseBranch {..} = do
+    pat <- ppCode _caseBranchPattern
+    body <- ppCode _caseBranchBody
+    return $ pat <+> arrow <+> body
+
+instance PrettyCode Pattern where
+  ppCode = \case
+    PatVar x -> ppCode x
+    PatConstrApp x -> ppCode x
+
+instance PrettyCode ConstrApp where
+  ppCode ConstrApp {..} = do
+    args <- mapM ppCode _constrAppArgs
+    name <- ppCode _constrAppConstructor
+    return $ (if null args then id else parens) $ name <+> hsep args
+
+instance PrettyCode Lambda where
+  ppCode Lambda {..} = do
+    name <- ppCode _lambdaVar
+    ty <- ppCode _lambdaType
+    body <- ppCode _lambdaBody
+    return $ parens $ kwLambda <+> name <+> colon <> colon <+> ty <+> dot <+> body
+
 instance PrettyCode Statement where
   ppCode = \case
     StmtDefinition x -> ppCode x
@@ -73,13 +140,16 @@ instance PrettyCode Definition where
   ppCode Definition {..} = do
     n <- ppCode _definitionName
     ty <- ppCodeQuoted _definitionType
-    return $ kwDefinition <+> n <+> "::" <+> ty <+> kwWhere <> line <> dquotes (n <+> "=" <+> kwUndefined)
+    body <- ppCode _definitionBody
+    return $ kwDefinition <+> n <+> "::" <+> ty <+> kwWhere <> line <> dquotes (n <+> "=" <+> body)
 
 instance PrettyCode Function where
   ppCode Function {..} = do
     n <- ppCode _functionName
     ty <- ppCodeQuoted _functionType
-    return $ kwFun <+> n <+> "::" <+> ty <+> kwWhere <> line <> dquotes (n <+> "_" <+> "=" <+> kwUndefined)
+    args <- mapM ppCode _functionArgs
+    body <- ppCode _functionBody
+    return $ kwFun <+> n <+> "::" <+> ty <+> kwWhere <> line <> dquotes (n <+> hsep args <+> "=" <+> body)
 
 instance PrettyCode Synonym where
   ppCode Synonym {..} = do
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
index 553c37d59e..25c6e37854 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
@@ -28,3 +28,12 @@ kwImports = keyword "imports"
 
 kwBegin :: Doc Ann
 kwBegin = keyword "begin"
+
+kwIf :: Doc Ann
+kwIf = keyword "if"
+
+kwThen :: Doc Ann
+kwThen = keyword "then"
+
+kwElse :: Doc Ann
+kwElse = keyword "else"