Lean 4 Tut

Posted on August 2, 2019
Tags: lean

1 Lists

#check [1,2,3]

1.1 Arrays

#check #[1,2,3]

2 Pattern matching and Functors,Monads,Applicative

Angled brackets \< \> lets us extract items from a constructor aka pattern matching

namespace patternMatched
inductive myId (T : Type)
  | id' : T -> myId T

open myId

instance: Functor myId where
  map := λ f (id' a) => id' $ f a

instance: Applicative myId where
  pure x := id' x 
  seq f x := match f with 
              | (id' g) => match x () with 
                            | (id' y) => id' (g y)
                            
instance: Monad myId where
  bind := λ a f => match a with
                    | (id' x) => f x


end patternMatched
namespace angledBrackets

inductive myId (T : Type)
  | id' : T -> myId T

open myId

instance: Functor myId where 
  map := λ f ⟨ a ⟩ => id' $ f a

instance: Applicative myId where
  pure x := id' x 
  seq := λ ⟨g⟩ x => match x () with | ⟨ y ⟩  => id' (g y) 

instance: Monad myId where
  bind := λ ⟨x⟩ => λ f => f x

end angledBrackets