equal
deleted
inserted
replaced
730 |
730 |
731 @{ML_response_fake [display,gray] |
731 @{ML_response_fake [display,gray] |
732 "lambda @{term \"x::nat\"} @{term \"(P::nat\<Rightarrow>bool) x\"}" |
732 "lambda @{term \"x::nat\"} @{term \"(P::nat\<Rightarrow>bool) x\"}" |
733 "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"} |
733 "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"} |
734 |
734 |
735 In the example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), |
735 In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), |
736 and an abstraction. It also records the type of the abstracted |
736 and an abstraction. It also records the type of the abstracted |
737 variable and for printing purposes also its name. Note that because of the |
737 variable and for printing purposes also its name. Note that because of the |
738 typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"} |
738 typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"} |
739 is of the same type as the abstracted variable. If it is of different type, |
739 is of the same type as the abstracted variable. If it is of different type, |
740 as in |
740 as in |