kbuzzard

import algebra.ring 

structure pre_semi_sheaf_of_rings (α : Type) := 
(F : Π (U : set α), Type)
[Fring : ∀ (U : set α), comm_ring (F U)]

attribute [instance] pre_semi_sheaf_of_rings.Fring

structure morphism_of_pre_semi_sheaves_of_rings {α : Type}
  (FPT : pre_semi_sheaf_of_rings α) (GPT : pre_semi_sheaf_of_rings α) :=

kbuzzard

import algebra.ring 

structure pre_semi_sheaf_of_rings (α : Type) := 
(F : Π (U : set α), Type)
[Fring : ∀ (U : set α), comm_ring (F U)]

attribute [instance] pre_semi_sheaf_of_rings.Fring

structure morphism_of_pre_semi_sheaves_of_rings {α : Type}
  (FPT : pre_semi_sheaf_of_rings α) (GPT : pre_semi_sheaf_of_rings α) :=

kbuzzard

scratch5.lean:393:0: information trace output
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_2 : @module ?x_0 (Π (i : ι), E i) ?x_1 := @pi.module ?x_3 ?x_4 ?x_5 ?x_6 ?x_7
[class_instances] (1) ?x_6 : ring ?x_5 := @prod.ring ?x_8 ?x_9 ?x_10 ?x_11
failed is_def_eq
[class_instances] (1) ?x_6 : ring ?x_5 := @normed_ring.to_ring ?x_12 ?x_13
[class_instances] (2) ?x_13 : normed_ring ?x_12 := @normed_field.to_normed_ring ?x_14 ?x_15
[class_instances] (3) ?x_15 : normed_field ?x_14 := _inst_1
[class_instances] (1) ?x_7 i : @module α (E i) (@normed_ring.to_ring α (@normed_field.to_normed_ring α _inst_1)) := @pi.module (?x_16 i) (?x_17 i) (?x_18 i) (?x_19 i) (?x_20 i)
failed is_def_eq

kbuzzard

import data.nat.prime 

namespace nat

definition Prime := subtype prime

-- unit test

definition two' : Prime := ⟨2,prime_two⟩

kbuzzard

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @topological_add_monoid (Π (i : γ), F i) (@Pi.topological_space γ (λ (i : γ), F i) (λ (a : γ), _inst_1 a))
  (@add_group.to_add_monoid (Π (i : γ), F i) (@pi.add_group γ (λ (i : γ), F i) (λ (i : γ), _inst_2 i))) := @topological_ring.to_topological_add_monoid ?x_1 ?x_2 ?x_3 ?x_4
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_5 : ring (Π (i : γ), F i) := @pi.ring ?x_6 ?x_7 ?x_8
[class_instances] (1) ?x_8 i : ring (F i) := @pi.ring (?x_9 i) (?x_10 i) (?x_11 i)
failed is_def_eq
[class_instances] (1) ?x_8 i : ring (F i) := @nonneg_ring.to_ring (?x_12 i) (?x_13 i)
[class_instances] (2) ?x_13 i : nonneg_ring (F i) := @linear_nonneg_ring.to_nonneg_ring (?x_14 i) (?x_15 i)
[class_instances] (1) ?x_8 i : ring (F i) := @domain.to_ring (?x_9 i) (?x_10 i)

kbuzzard

import data.equiv 

def is_valuation {R : Type} [comm_ring R] {α : Type} [linear_order α] (f : R → α) : Prop := true

structure valuations (R : Type) [comm_ring R] :=
(α : Type) [Hα : linear_order α] (f : R → α) (Hf : is_valuation f)

instance to_make_next_line_work (R : Type) [comm_ring R] (v : valuations R) : linear_order v.α := v.Hα

instance valuations.setoid (R : Type) [comm_ring R] : setoid (valuations R) := {

kbuzzard

definition X := some 0 

#check X

#check ℕ

#check option 

#check some

kbuzzard

definition X := some 0 

#check X

#check ℕ

#check option 

#check some

kbuzzard

-- Church numerals

-- Another way of doing nat.

-- The church nat, chℕ (happy to change the name) is a pi type
-- and not a structure. So proofs are not done by induction!
--import data.equiv 

def chℕ := Π X : Type, (X → X) → X → X 

kbuzzard

c : ℕ,
h : c ≥ 3
⊢ N_min
      (pmap
           (λ (a : ℕ) (h : a ∈ c :: 0),
              a - 2 +
                int.nat_abs
                  (2 -
                     ↑((λ (t : multiset ℕ) (h : t < c :: 0),
                           strong_induction_on t