benediktahrens

# tlp-stat
--- TLP 1.5.0 --------------------------------------------

+++ Configured Settings:
/etc/tlp.conf L0029: TLP_ENABLE="1"
defaults.conf L0005: TLP_WARN_LEVEL="3"
defaults.conf L0006: TLP_PERSISTENT_DEFAULT="0"
defaults.conf L0007: DISK_IDLE_SECS_ON_AC="0"
defaults.conf L0008: DISK_IDLE_SECS_ON_BAT="2"
defaults.conf L0009: MAX_LOST_WORK_SECS_ON_AC="15"

benediktahrens

# tlp-stat --cdiff -s -b
--- TLP 1.5.0 --------------------------------------------

+++ Configured Settings (only differences to defaults):
/etc/tlp.conf L0044: TLP_DEFAULT_MODE="BAT"
/etc/tlp.conf L0087: CPU_SCALING_GOVERNOR_ON_AC="powersave"
/etc/tlp.conf L0088: CPU_SCALING_GOVERNOR_ON_BAT="powersave"
/etc/tlp.conf L0099: CPU_SCALING_MIN_FREQ_ON_AC="0"
/etc/tlp.conf L0100: CPU_SCALING_MAX_FREQ_ON_AC="0"
/etc/tlp.conf L0101: CPU_SCALING_MIN_FREQ_ON_BAT="0"

benediktahrens

# ------------------------------------------------------------------------------
# /etc/tlp.conf - TLP user configuration (version 1.4)
# See full explanation: https://linrunner.de/tlp/settings
#
# Settings are read in the following order:
#
# 1. Intrinsic defaults
# 2. /etc/tlp.d/*.conf - Drop-in customization snippets
# 3. /etc/tlp.conf     - User configuration (this file)
#

benediktahrens

import data.sum  --for sum.elim
import logic.basic --for empty.elim
open sum


section exercise_1a

variables A B : Prop

example : A ∧ B → B ∧ A :=

benediktahrens

import data.sum  --for sum.elim
import logic.basic --for empty.elim
open sum


section foo

variables A B : Prop

example : A ∧ B → B ∧ A := _

benediktahrens

section exercise1

variable U : Type
variables A B C: U → Prop

example (h : ∀ x, A x → B x)
        (k : ∃ x, A x)

benediktahrens

/-
Lecture 23:

Predicate logic
     ---
  ∃ in Lean


Contents:

benediktahrens

/-
Lecture 21:

Predicate logic
     ---
first proofs in Lean


Contents:

benediktahrens

/-
Lecture 18:

Predicate logic
     ---
first steps in Lean


Contents:

benediktahrens

/-
Lecture 18:

Predicate logic
     ---
first steps in Lean


Contents: