Idris2/samples/holes.idr

mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 02:31:50 +03:00
main : IO ()
main = putStrLn ?greeting

even : Nat -> Bool
even Z = True
even (S k) = ?even_rhs
Copy samples directory from Idris2-boot This is referred to in the documentation, so should be there 2020-06-30 12:51:09 +03:00			`main : IO ()`
			`main = putStrLn ?greeting`

			`even : Nat -> Bool`
			`even Z = True`
			`even (S k) = ?even_rhs`