PatrickMassot

{
	"Type*": {
                "prefix": "Type*",
                "body": [
                  "{$1 : Type*}$0"
                ],
        "description": "Type* variable",
        },
        "Variables": {
                "prefix": "var",

PatrickMassot

/-
This file is intended for Lean beginners. The goal is to demonstrate what it feels like to prove
things using Lean and mathlib. Complicated definitions and theory building are not covered.
-/

-- We want real numbers and their basic properties
import data.real.basic

-- We want to be able to define functions using the law of excluded middle
local attribute [instance, priority 0] classical.prop_decidable