chore(*): cleanup
This commit is contained in:
Leonardo de Moura
parent
2946174c1e
commit
080c2dabde
1767 changed files with 0 additions and 31706 deletions
|
|
@ -1,47 +0,0 @@
|
|||
lstlean.tex
|
||||
===========
|
||||
|
||||
The file `lstlean.tex` contains /Lean/ style definitions for the
|
||||
`listings` package, which can be used to typeset Lean code in a
|
||||
Latex document. For more information, see the documentation for the
|
||||
`listings` package and the sample document `sample.tex`.
|
||||
|
||||
You need the following packages installed:
|
||||
|
||||
- `listings`
|
||||
- `inputenc`
|
||||
- `color`
|
||||
|
||||
Because `listings` does not work well with unicode, the style
|
||||
replaces all unicode characters with Latex equivalents. Some of the
|
||||
replacment symbols require the `amssymb` package.
|
||||
|
||||
To use the style, all you need to do is include `lstlean.tex` in
|
||||
the same directory as your Latex source, and include the following
|
||||
preamble in your document:
|
||||
```
|
||||
\documentclass{article}
|
||||
|
||||
\usepackage[utf8x]{inputenc}
|
||||
\usepackage{amssymb}
|
||||
|
||||
\usepackage{color}
|
||||
\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1} % red
|
||||
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4} % grey
|
||||
\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6} % blue
|
||||
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1} % green
|
||||
|
||||
\usepackage{listings}
|
||||
\def\lstlanguagefiles{lstlean.tex}
|
||||
\lstset{language=lean}
|
||||
```
|
||||
|
||||
The `inputenc` package is needed to handle unicode input. Of
|
||||
course, you can set the colors any way you want. In your document,
|
||||
you can then in-line code with the `\lstinline{...}`, and add a code
|
||||
block with the `\begin{lstlisting} ... \end{lstlisting}`
|
||||
environment.
|
||||
|
||||
Note that if you use a unicode symbol that is not currently handled in
|
||||
`lstlean.tex`, you can simply add it to the list there, together
|
||||
with the Latex equivalent you would like to use.
|
||||
|
|
@ -1,276 +0,0 @@
|
|||
% Listing style definition for the Lean Theorem Prover.
|
||||
% Defined by Jeremy Avigad, 2015, by modifying Assia Mahboubi's SSR style.
|
||||
% Unicode replacements taken from Olivier Verdier's unixode.sty
|
||||
|
||||
\lstdefinelanguage{lean} {
|
||||
|
||||
% Anything betweeen $ becomes LaTeX math mode
|
||||
mathescape=true,
|
||||
% Comments may or not include Latex commands
|
||||
texcl=false,
|
||||
|
||||
% keywords, list taken from lean-syntax.el
|
||||
morekeywords=[1]{
|
||||
import, prelude, protected, private, noncomputable, definition, meta, renaming,
|
||||
hiding, exposing, parameter, parameters, begin, conjecture, constant, constants,
|
||||
hypothesis, lemma, corollary, variable, variables, premise, premises, theory,
|
||||
print, theorem, proposition, example, abstract,
|
||||
open, as, export, override, axiom, axioms, inductive, with, without,
|
||||
structure, record, universe, universes,
|
||||
alias, help, precedence, reserve, declare_trace, add_key_equivalence,
|
||||
match, infix, infixl, infixr, notation, postfix, prefix, instance,
|
||||
eval, vm_eval, check, coercion, end, this, suppose,
|
||||
using, using_well_founded, namespace, section, fields,
|
||||
attribute, local, set_option, extends, include, omit, classes, class,
|
||||
instances, coercions, attributes, raw, replacing,
|
||||
calc, have, show, suffices, by, in, at, let, forall, Pi, fun,
|
||||
exists, if, dif, then, else, assume, take, obtain, from, aliases, register_simp_ext,
|
||||
mutual, def, run_command
|
||||
},
|
||||
|
||||
% Sorts
|
||||
morekeywords=[2]{Type, Prop, Type*, Type₀, Type₁, Type₂, Type₃},
|
||||
|
||||
% tactics, list taken from lean-syntax.el
|
||||
% morekeywords=[3]{
|
||||
% Cond, or_else, then, try, when, assumption, eassumption, rapply,
|
||||
% apply, fapply, eapply, rename, intro, intros, all_goals, fold, focus, focus_at,
|
||||
% generalize, generalizes, clear, clears, revert, reverts, back, beta, done, exact, rexact,
|
||||
% refine, repeat, whnf, rotate, rotate_left, rotate_right, inversion, cases, rewrite,
|
||||
% xrewrite, krewrite, blast, simp, esimp, unfold, change, check_expr, contradiction,
|
||||
% exfalso, split, existsi, constructor, fconstructor, left, right, injection, congruence, reflexivity,
|
||||
% symmetry, transitivity, state, induction, induction_using, fail, append,
|
||||
% substvars, now, with_options, with_attributes, with_attrs, note
|
||||
% },
|
||||
|
||||
% modifiers, taken from lean-syntax.el
|
||||
% note: 'otherkeywords' is needed because these use a different symbol.
|
||||
% this command doesn't allow us to specify a number -- they are put with [1]
|
||||
% otherkeywords={
|
||||
% [persistent], [notation], [visible], [instance], [trans_instance],
|
||||
% [class], [parsing-only], [coercion], [unfold_full], [constructor],
|
||||
% [reducible], [irreducible], [semireducible], [quasireducible], [wf],
|
||||
% [whnf], [multiple_instances], [none], [decl], [declaration],
|
||||
% [relation], [symm], [subst], [refl], [trans], [simp], [congr], [unify],
|
||||
% [backward], [forward], [no_pattern], [begin_end], [tactic], [abbreviation],
|
||||
% [reducible], [unfold], [alias], [eqv], [intro], [intro!], [elim], [grinder],
|
||||
% [localrefinfo], [recursor]
|
||||
% },
|
||||
|
||||
% Various symbols
|
||||
literate=
|
||||
{α}{{\ensuremath{\mathrm{\alpha}}}}1
|
||||
{β}{{\ensuremath{\mathrm{\beta}}}}1
|
||||
{γ}{{\ensuremath{\mathrm{\gamma}}}}1
|
||||
{δ}{{\ensuremath{\mathrm{\delta}}}}1
|
||||
{ε}{{\ensuremath{\mathrm{\varepsilon}}}}1
|
||||
{ζ}{{\ensuremath{\mathrm{\zeta}}}}1
|
||||
{η}{{\ensuremath{\mathrm{\eta}}}}1
|
||||
{θ}{{\ensuremath{\mathrm{\theta}}}}1
|
||||
{ι}{{\ensuremath{\mathrm{\iota}}}}1
|
||||
{κ}{{\ensuremath{\mathrm{\kappa}}}}1
|
||||
{μ}{{\ensuremath{\mathrm{\mu}}}}1
|
||||
{ν}{{\ensuremath{\mathrm{\nu}}}}1
|
||||
{ξ}{{\ensuremath{\mathrm{\xi}}}}1
|
||||
{π}{{\ensuremath{\mathrm{\mathnormal{\pi}}}}}1
|
||||
{ρ}{{\ensuremath{\mathrm{\rho}}}}1
|
||||
{σ}{{\ensuremath{\mathrm{\sigma}}}}1
|
||||
{τ}{{\ensuremath{\mathrm{\tau}}}}1
|
||||
{φ}{{\ensuremath{\mathrm{\varphi}}}}1
|
||||
{χ}{{\ensuremath{\mathrm{\chi}}}}1
|
||||
{ψ}{{\ensuremath{\mathrm{\psi}}}}1
|
||||
{ω}{{\ensuremath{\mathrm{\omega}}}}1
|
||||
|
||||
{Γ}{{\ensuremath{\mathrm{\Gamma}}}}1
|
||||
{Δ}{{\ensuremath{\mathrm{\Delta}}}}1
|
||||
{Θ}{{\ensuremath{\mathrm{\Theta}}}}1
|
||||
{Λ}{{\ensuremath{\mathrm{\Lambda}}}}1
|
||||
{Σ}{{\ensuremath{\mathrm{\Sigma}}}}1
|
||||
{Φ}{{\ensuremath{\mathrm{\Phi}}}}1
|
||||
{Ξ}{{\ensuremath{\mathrm{\Xi}}}}1
|
||||
{Ψ}{{\ensuremath{\mathrm{\Psi}}}}1
|
||||
{Ω}{{\ensuremath{\mathrm{\Omega}}}}1
|
||||
|
||||
{ℵ}{{\ensuremath{\aleph}}}1
|
||||
|
||||
{≤}{{\ensuremath{\leq}}}1
|
||||
{≥}{{\ensuremath{\geq}}}1
|
||||
{≠}{{\ensuremath{\neq}}}1
|
||||
{≈}{{\ensuremath{\approx}}}1
|
||||
{≡}{{\ensuremath{\equiv}}}1
|
||||
{≃}{{\ensuremath{\simeq}}}1
|
||||
|
||||
{≤}{{\ensuremath{\leq}}}1
|
||||
{≥}{{\ensuremath{\geq}}}1
|
||||
|
||||
{∂}{{\ensuremath{\partial}}}1
|
||||
{∆}{{\ensuremath{\triangle}}}1 % or \laplace?
|
||||
|
||||
{∫}{{\ensuremath{\int}}}1
|
||||
{∑}{{\ensuremath{\mathrm{\Sigma}}}}1
|
||||
{Π}{{\ensuremath{\mathrm{\Pi}}}}1
|
||||
|
||||
{⊥}{{\ensuremath{\perp}}}1
|
||||
{∞}{{\ensuremath{\infty}}}1
|
||||
{∂}{{\ensuremath{\partial}}}1
|
||||
|
||||
{∓}{{\ensuremath{\mp}}}1
|
||||
{±}{{\ensuremath{\pm}}}1
|
||||
{×}{{\ensuremath{\times}}}1
|
||||
|
||||
{⊕}{{\ensuremath{\oplus}}}1
|
||||
{⊗}{{\ensuremath{\otimes}}}1
|
||||
{⊞}{{\ensuremath{\boxplus}}}1
|
||||
|
||||
{∇}{{\ensuremath{\nabla}}}1
|
||||
{√}{{\ensuremath{\sqrt}}}1
|
||||
|
||||
{⬝}{{\ensuremath{\cdot}}}1
|
||||
{•}{{\ensuremath{\cdot}}}1
|
||||
{∘}{{\ensuremath{\circ}}}1
|
||||
|
||||
%{⁻}{{\ensuremath{^{\textup{\kern1pt\rule{2pt}{0.3pt}\kern-1pt}}}}}1
|
||||
{⁻}{{\ensuremath{^{-}}}}1
|
||||
{▸}{{\ensuremath{\blacktriangleright}}}1
|
||||
|
||||
{∧}{{\ensuremath{\wedge}}}1
|
||||
{∨}{{\ensuremath{\vee}}}1
|
||||
{¬}{{\ensuremath{\neg}}}1
|
||||
{⊢}{{\ensuremath{\vdash}}}1
|
||||
|
||||
%{⟨}{{\ensuremath{\left\langle}}}1
|
||||
%{⟩}{{\ensuremath{\right\rangle}}}1
|
||||
{⟨}{{\ensuremath{\langle}}}1
|
||||
{⟩}{{\ensuremath{\rangle}}}1
|
||||
|
||||
{↦}{{\ensuremath{\mapsto}}}1
|
||||
{→}{{\ensuremath{\rightarrow}}}1
|
||||
{↔}{{\ensuremath{\leftrightarrow}}}1
|
||||
{⇒}{{\ensuremath{\Rightarrow}}}1
|
||||
{⟹}{{\ensuremath{\Longrightarrow}}}1
|
||||
{⇐}{{\ensuremath{\Leftarrow}}}1
|
||||
{⟸}{{\ensuremath{\Longleftarrow}}}1
|
||||
|
||||
{∩}{{\ensuremath{\cap}}}1
|
||||
{∪}{{\ensuremath{\cup}}}1
|
||||
{⊂}{{\ensuremath{\subseteq}}}1
|
||||
{⊆}{{\ensuremath{\subseteq}}}1
|
||||
{⊄}{{\ensuremath{\nsubseteq}}}1
|
||||
{⊈}{{\ensuremath{\nsubseteq}}}1
|
||||
{⊃}{{\ensuremath{\supseteq}}}1
|
||||
{⊇}{{\ensuremath{\supseteq}}}1
|
||||
{⊅}{{\ensuremath{\nsupseteq}}}1
|
||||
{⊉}{{\ensuremath{\nsupseteq}}}1
|
||||
{∈}{{\ensuremath{\in}}}1
|
||||
{∉}{{\ensuremath{\notin}}}1
|
||||
{∋}{{\ensuremath{\ni}}}1
|
||||
{∌}{{\ensuremath{\notni}}}1
|
||||
{∅}{{\ensuremath{\emptyset}}}1
|
||||
|
||||
{∖}{{\ensuremath{\setminus}}}1
|
||||
{†}{{\ensuremath{\dag}}}1
|
||||
|
||||
{ℕ}{{\ensuremath{\mathbb{N}}}}1
|
||||
{ℤ}{{\ensuremath{\mathbb{Z}}}}1
|
||||
{ℝ}{{\ensuremath{\mathbb{R}}}}1
|
||||
{ℚ}{{\ensuremath{\mathbb{Q}}}}1
|
||||
{ℂ}{{\ensuremath{\mathbb{C}}}}1
|
||||
{⌞}{{\ensuremath{\llcorner}}}1
|
||||
{⌟}{{\ensuremath{\lrcorner}}}1
|
||||
{⦃}{{\ensuremath{\{\!|}}}1
|
||||
{⦄}{{\ensuremath{|\!\}}}}1
|
||||
|
||||
{₁}{{\ensuremath{_1}}}1
|
||||
{₂}{{\ensuremath{_2}}}1
|
||||
{₃}{{\ensuremath{_3}}}1
|
||||
{₄}{{\ensuremath{_4}}}1
|
||||
{₅}{{\ensuremath{_5}}}1
|
||||
{₆}{{\ensuremath{_6}}}1
|
||||
{₇}{{\ensuremath{_7}}}1
|
||||
{₈}{{\ensuremath{_8}}}1
|
||||
{₉}{{\ensuremath{_9}}}1
|
||||
{₀}{{\ensuremath{_0}}}1
|
||||
|
||||
{¹}{{\ensuremath{^1}}}1
|
||||
|
||||
{ₙ}{{\ensuremath{_n}}}1
|
||||
{ₘ}{{\ensuremath{_m}}}1
|
||||
{↑}{{\ensuremath{\uparrow}}}1
|
||||
{↓}{{\ensuremath{\downarrow}}}1
|
||||
|
||||
{▸}{{\ensuremath{\triangleright}}}1
|
||||
|
||||
{Σ}{{\color{symbolcolor}\ensuremath{\Sigma}}}1
|
||||
{Π}{{\color{symbolcolor}\ensuremath{\Pi}}}1
|
||||
{∀}{{\color{symbolcolor}\ensuremath{\forall}}}1
|
||||
{∃}{{\color{symbolcolor}\ensuremath{\exists}}}1
|
||||
{λ}{{\color{symbolcolor}\ensuremath{\mathrm{\lambda}}}}1
|
||||
|
||||
{:=}{{\color{symbolcolor}:=}}1
|
||||
{=}{{\color{symbolcolor}=}}1
|
||||
{<}{{\color{symbolcolor}<}}1
|
||||
{+}{{\color{symbolcolor}+}}1
|
||||
{*}{{\color{symbolcolor}*}}1,
|
||||
|
||||
% Comments
|
||||
%comment=[s][\itshape \color{commentcolor}]{/-}{-/},
|
||||
morecomment=[s][\color{commentcolor}]{/-}{-/},
|
||||
morecomment=[l][\itshape \color{commentcolor}]{--},
|
||||
|
||||
% Spaces are not displayed as a special character
|
||||
showstringspaces=false,
|
||||
|
||||
% keep spaces
|
||||
keepspaces=true,
|
||||
|
||||
% String delimiters
|
||||
morestring=[b]",
|
||||
morestring=[d],
|
||||
|
||||
% Size of tabulations
|
||||
tabsize=3,
|
||||
|
||||
% Enables ASCII chars 128 to 255
|
||||
extendedchars=false,
|
||||
|
||||
% Case sensitivity
|
||||
sensitive=true,
|
||||
|
||||
% Automatic breaking of long lines
|
||||
breaklines=true,
|
||||
|
||||
% Default style fors listingsred
|
||||
basicstyle=\ttfamily,
|
||||
|
||||
% Position of captions is bottom
|
||||
captionpos=b,
|
||||
|
||||
% Full flexible columns
|
||||
columns=[l]fullflexible,
|
||||
|
||||
|
||||
% Style for (listings') identifiers
|
||||
identifierstyle={\ttfamily\color{black}},
|
||||
% Note : highlighting of Coq identifiers is done through a new
|
||||
% delimiter definition through an lstset at the begining of the
|
||||
% document. Don't know how to do better.
|
||||
|
||||
% Style for declaration keywords
|
||||
keywordstyle=[1]{\ttfamily\color{keywordcolor}},
|
||||
|
||||
% Style for sorts
|
||||
keywordstyle=[2]{\ttfamily\color{sortcolor}},
|
||||
|
||||
% Style for tactics keywords
|
||||
% keywordstyle=[3]{\ttfamily\color{tacticcolor}},
|
||||
|
||||
% Style for attributes
|
||||
% keywordstyle=[4]{\ttfamily\color{attributecolor}},
|
||||
|
||||
% Style for strings
|
||||
stringstyle=\ttfamily,
|
||||
|
||||
% Style for comments
|
||||
% commentstyle={\ttfamily\footnotesize },
|
||||
|
||||
}
|
||||
|
|
@ -1,71 +0,0 @@
|
|||
\documentclass{article}
|
||||
|
||||
\usepackage[utf8x]{inputenc}
|
||||
\usepackage{amssymb}
|
||||
|
||||
\usepackage{color}
|
||||
\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1} % red
|
||||
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4} % grey
|
||||
\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6} % blue
|
||||
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1} % green
|
||||
|
||||
\usepackage{listings}
|
||||
\def\lstlanguagefiles{lstlean.tex}
|
||||
\lstset{language=lean}
|
||||
|
||||
\title{The Lean listing style}
|
||||
\author{Jeremy Avigad}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\maketitle
|
||||
|
||||
This is an example of how to use \verb=lstlean.tex= to typeset your Lean code. Here is some code: \lstinline{theorem foo (x y : ℕ), x + y = y + x}. Here are the translations of some unicode symbols:
|
||||
\begin{lstlisting}
|
||||
Some symbols: ℕ ℤ ∩ ⊂ ∀ ∃ Π α β γ ∈ ⦃ ⦄
|
||||
\end{lstlisting}
|
||||
Here is a block of code:
|
||||
\begin{lstlisting}
|
||||
/-
|
||||
Basic properties of lists.
|
||||
-/
|
||||
|
||||
inductive list (α : Type) : Type
|
||||
| nil {} : list
|
||||
| cons : α → list → list
|
||||
|
||||
namespace list
|
||||
|
||||
notation h :: t := cons h t
|
||||
notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
|
||||
|
||||
variable {α : Type}
|
||||
|
||||
/- append -/
|
||||
|
||||
def append : list α → list α → list α
|
||||
| [] l := l
|
||||
| (h :: s) t := h :: (append s t)
|
||||
|
||||
notation l₁ ++ l₂ := append l₁ l₂
|
||||
|
||||
theorem nil_append (t : list α) : [] ++ t = t := rfl
|
||||
|
||||
theorem append_cons (x : α) (s t : list α) : (x::s) ++ t = x::(s ++ t) := rfl
|
||||
|
||||
theorem append_nil : ∀ (t : list α), t ++ [] = t
|
||||
| [] := rfl
|
||||
| (a :: l) := calc
|
||||
(a :: l) ++ [] = a :: (l ++ []) : rfl
|
||||
... = a :: l : by rw append_nil l
|
||||
|
||||
theorem append.assoc : ∀ (s t u : list α), s ++ t ++ u = s ++ (t ++ u)
|
||||
| [] t u := rfl
|
||||
| (a :: l) t u :=
|
||||
show a :: (l ++ t ++ u) = (a :: l) ++ (t ++ u),
|
||||
begin rw (append.assoc l t u), reflexivity end
|
||||
|
||||
end list
|
||||
\end{lstlisting}
|
||||
|
||||
\end{document}
|
||||
1
leanpkg/.gitignore
vendored
1
leanpkg/.gitignore
vendored
|
|
@ -1 +0,0 @@
|
|||
/leanpkg/config_vars.lean
|
||||
3
old_tests/tests/.gitignore
vendored
3
old_tests/tests/.gitignore
vendored
|
|
@ -1,3 +0,0 @@
|
|||
*.produced.out
|
||||
*.test_suite.out
|
||||
*.status
|
||||
1
old_tests/tests/lean/.gitignore
vendored
1
old_tests/tests/lean/.gitignore
vendored
|
|
@ -1 +0,0 @@
|
|||
io_fs.txt
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
inductive weekday : Type
|
||||
| sunday : weekday
|
||||
| monday : weekday
|
||||
| tuesday : weekday
|
||||
| wednesday : weekday
|
||||
|
||||
def ppday (d : weekday) : nat :=
|
||||
match d with
|
||||
| sunday := 0
|
||||
| monday := 1
|
||||
| tuesday := 2
|
||||
| wednesday := 3
|
||||
end
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
1162.lean:10:12: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
|
||||
1162.lean:11:12: error: equation compiler error, equation #3 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
|
||||
1162.lean:12:12: error: equation compiler error, equation #4 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
example : true :=
|
||||
begin
|
||||
have H : true := (by trivial),
|
||||
exact H
|
||||
end
|
||||
|
||||
example : true :=
|
||||
begin
|
||||
have H : true := (by tactic.triv),
|
||||
exact H
|
||||
end
|
||||
|
||||
meta example (h : tactic unit) : true :=
|
||||
begin
|
||||
h, -- ERROR h should not be visible here
|
||||
trivial
|
||||
end
|
||||
|
||||
example : false :=
|
||||
begin
|
||||
have H : true := (by foo), -- ERROR
|
||||
exact sorry
|
||||
end
|
||||
|
||||
constant P : Prop
|
||||
example (p : P) : true :=
|
||||
begin
|
||||
have H : P := by do { p ← tactic.get_local `p, tactic.exact p },
|
||||
trivial
|
||||
end
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
1207.lean:15:2: error: unknown identifier 'h'
|
||||
1207.lean:15:2: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
h : tactic unit,
|
||||
_example : true
|
||||
⊢ Type ?
|
||||
1207.lean:21:23: error: unknown identifier 'foo'
|
||||
1207.lean:21:23: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
⊢ Type ?
|
||||
state:
|
||||
⊢ false
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
constant P : list ℕ → list ℕ → Prop
|
||||
lemma foo (xs : list ℕ) : Π (ns : list ℕ), P xs ns
|
||||
| [] := sorry
|
||||
| (n::ns) := begin cases xs, exact sorry, exact sorry end
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
1258.lean:4:19: error: failed to revert 'xs', 'foo' depends on it, and 'foo' is an auxiliary declaration introduced by the equation compiler (possible solution: use tactic 'clear' to remove 'foo' from the local context)
|
||||
state:
|
||||
xs : list ℕ,
|
||||
foo : ∀ (ns : list ℕ), P xs ns,
|
||||
n : ℕ,
|
||||
ns : list ℕ
|
||||
⊢ P xs (n :: ns)
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
variables {α₁ : Type} {α₂ : α₁ → Type} {β₁ : Type} {β₂ : β₁ → Type}
|
||||
|
||||
def map (f₁ : α₁ → β₁) (f₂ : Π⦃a⦄, α₂ a → β₂ (f₁ a)) : (Σa, α₂ a) → (Σb, β₂ b)
|
||||
| ⟨a₁, a₂⟩ := ⟨f₁ a₁, f₂ a₂⟩
|
||||
|
||||
example (f₁ : α₁ → α₁) (f₂ : Π⦃a⦄, α₂ a → α₂ (f₁ a)) (eq₁ : f₁ = id) : map f₁ f₂ = id :=
|
||||
begin
|
||||
rw [eq₁],
|
||||
end
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
1277.lean:8:2: error: rewrite tactic failed, motive is not type correct
|
||||
nested exception message:
|
||||
check failed, application type mismatch (use 'set_option trace.check true' for additional details)
|
||||
state:
|
||||
α₁ : Type,
|
||||
α₂ : α₁ → Type,
|
||||
f₁ : α₁ → α₁,
|
||||
f₂ : Π ⦃a : α₁⦄, α₂ a → α₂ (f₁ a),
|
||||
eq₁ : f₁ = id
|
||||
⊢ map f₁ f₂ = id
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
structure Category : Type 2 :=
|
||||
(Obj : Type)
|
||||
(Hom : Obj → Obj → Type)
|
||||
(compose : Π ⦃A B C : Obj⦄, Hom A B → Hom B C → Hom A C)
|
||||
|
||||
open Category
|
||||
|
||||
structure Functor (source target : Category) : Type :=
|
||||
(onObjects : Obj source → Obj target)
|
||||
(onMorphisms : Π ⦃A B : Obj source⦄, Hom source A B → Hom target (onObjects A) (onObjects B))
|
||||
(functoriality : Π ⦃A B C : Obj source⦄ (f : Hom source A B) (g : Hom source B C),
|
||||
onMorphisms (compose source g f) = compose target (onMorphisms g) (onMorphisms f))
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
1279.lean:12:33: error: type mismatch at application
|
||||
source.compose g f
|
||||
term
|
||||
f
|
||||
has type
|
||||
source.Hom A B
|
||||
but is expected to have type
|
||||
source.Hom C ?m_1
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
structure Category :=
|
||||
(Obj : Type)
|
||||
(Hom : Obj -> Obj -> Type)
|
||||
|
||||
structure Isomorphism ( C: Category ) { A B : C^.Obj } :=
|
||||
(morphism : C^.Hom A B)
|
||||
|
||||
instance Isomorphism_coercion_to_morphism { C : Category } { A B C^.Obj } : has_coe (Isomorphism C A B) (C^.Hom A B) :=
|
||||
(coe: Isomorphism.morphism)
|
||||
|
||||
instance Isomorphism_coercion_to_morphism_fixed { C : Category } { A B : C^.Obj } : has_coe (Isomorphism C) (C^.Hom A B) :=
|
||||
{coe := Isomorphism.morphism}
|
||||
|
|
@ -1,31 +0,0 @@
|
|||
1290.lean:8:66: error: invalid declaration, '}' expected
|
||||
1290.lean:8:61: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
C : Category
|
||||
⊢ Sort ?
|
||||
1290.lean:8:63: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
C : Category,
|
||||
A : ⁇
|
||||
⊢ Sort ?
|
||||
1290.lean:8:65: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
C : Category,
|
||||
A : ⁇,
|
||||
B : ⁇
|
||||
⊢ Sort ?
|
||||
1290.lean:8:9: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
C : Category,
|
||||
A : ⁇,
|
||||
B : ⁇,
|
||||
C : ⁇
|
||||
⊢ Sort ?
|
||||
1290.lean:8:9: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
C : Category,
|
||||
A : ⁇,
|
||||
B : ⁇,
|
||||
C : ⁇
|
||||
⊢ Sort ?
|
||||
1290.lean:8:66: error: command expected
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
def fn (n : nat) : nat :=
|
||||
match n with
|
||||
|
||||
#exit
|
||||
|
||||
theorem thm : true := begin end
|
||||
|
||||
example : has_add nat := sorry
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
1292.lean:4:0: error: invalid expression, unexpected token
|
||||
1292.lean:2:0: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
|
||||
1292.lean:4:0: warning: using 'exit' to interrupt Lean
|
||||
|
|
@ -1,15 +0,0 @@
|
|||
open expr tactic
|
||||
|
||||
example : true := by whnf (var 0) >> return ()
|
||||
|
||||
example : true := by whnf (app (var 0) (var 0)) >> return ()
|
||||
|
||||
example : true := by head_zeta (var 0) >> return ()
|
||||
|
||||
example : true := by unify (var 0) (var 0) >> return ()
|
||||
|
||||
example : true := by is_def_eq (var 0) (var 0) >> return ()
|
||||
|
||||
example (foo trivial) := by do
|
||||
t ← infer_type (var 0),
|
||||
to_expr ``(trivial) >>= apply
|
||||
|
|
@ -1,32 +0,0 @@
|
|||
1293.lean:3:21: error: tactic 'whnf' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
|
||||
state:
|
||||
⊢ true
|
||||
1293.lean:5:21: error: tactic 'whnf' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
|
||||
state:
|
||||
⊢ true
|
||||
1293.lean:7:21: error: tactic 'head_zeta' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
|
||||
state:
|
||||
⊢ true
|
||||
1293.lean:9:21: error: tactic 'unify' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
|
||||
state:
|
||||
⊢ true
|
||||
1293.lean:11:21: error: tactic 'is_def_eq' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
|
||||
state:
|
||||
⊢ true
|
||||
1293.lean:13:28: error: tactic 'infer_type' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
|
||||
state:
|
||||
foo : ?m_1,
|
||||
trivial : ?m_2
|
||||
⊢ ?m_3
|
||||
1293.lean:13:9: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
⊢ Sort ?
|
||||
1293.lean:13:13: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
foo : ⁇
|
||||
⊢ Sort ?
|
||||
1293.lean:13:8: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
foo : ⁇,
|
||||
trivial : ⁇
|
||||
⊢ Sort ?
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
open tactic expr
|
||||
|
||||
def d1 : true = true := by do
|
||||
trace (("a", "a")),
|
||||
prt ← to_expr ``(true = true),
|
||||
add_decl (declaration.ax `new_ax [] prt),
|
||||
l ← to_expr ```(new_ax),
|
||||
apply l
|
||||
|
||||
#check d1
|
||||
#print d1
|
||||
|
||||
theorem d2 : true = true := by do
|
||||
trace (("a", "a")),
|
||||
prt ← to_expr ``(true = true),
|
||||
add_decl (declaration.ax `new_ax2 [] prt),
|
||||
l ← to_expr ```(new_ax2),
|
||||
apply l
|
||||
|
||||
#print d2
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
(a, a)
|
||||
d1 : true = true
|
||||
def d1 : true = true :=
|
||||
new_ax
|
||||
(a, a)
|
||||
1299.lean:13:8: error: invalid theorem 'd2', theorems should not depend on axioms introduced using tactics (solution: mark theorem as a definition)
|
||||
theorem d2 : true = true :=
|
||||
⁇
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
example (n) : nat.pred n = n :=
|
||||
begin
|
||||
dsimp {fail_if_unchanged := ff}
|
||||
end
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
1327.lean:4:0: error: tactic failed, there are unsolved goals
|
||||
state:
|
||||
n : ℕ
|
||||
⊢ nat.pred n = n
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
inductive nlist : Type
|
||||
| atom : nlist
|
||||
| mk : list nlist → nlist
|
||||
|
||||
open nlist list
|
||||
|
||||
def fn : nlist → nlist
|
||||
| (mk l) := mk []
|
||||
| _ := atom
|
||||
|
||||
#check fn.equations._eqn_1
|
||||
#check fn.equations._eqn_2
|
||||
|
|
@ -1,2 +0,0 @@
|
|||
fn.equations._eqn_1 : fn atom = atom
|
||||
fn.equations._eqn_2 : ∀ (l : list nlist), fn (mk l) = mk nil
|
||||
|
|
@ -1,26 +0,0 @@
|
|||
inductive term : Type
|
||||
| var : nat → term
|
||||
| app : list term → term
|
||||
| cnst : string → term
|
||||
|
||||
def var_of : term → option nat
|
||||
| (term.var n) := some n
|
||||
| _ := none
|
||||
|
||||
#check var_of.equations._eqn_1
|
||||
#check var_of.equations._eqn_2
|
||||
#check var_of.equations._eqn_3
|
||||
|
||||
def list_of : term → list term
|
||||
| (term.app ts) := ts
|
||||
| _ := []
|
||||
|
||||
#check list_of.equations._eqn_1
|
||||
#check list_of.equations._eqn_2
|
||||
#check list_of.equations._eqn_3
|
||||
|
||||
example (a : nat) (ls : list term) : term.var a = term.app ls → false :=
|
||||
by contradiction
|
||||
|
||||
example (a : nat) (s : string) : ¬ term.var a = term.cnst s :=
|
||||
by contradiction
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
var_of.equations._eqn_1 : ∀ (n : ℕ), var_of (term.var n) = some n
|
||||
var_of.equations._eqn_2 : ∀ (a : list term), var_of (term.app a) = none
|
||||
var_of.equations._eqn_3 : ∀ (a : string), var_of (term.cnst a) = none
|
||||
list_of.equations._eqn_1 : ∀ (a : ℕ), list_of (term.var a) = list.nil
|
||||
list_of.equations._eqn_2 : ∀ (ts : list term), list_of (term.app ts) = ts
|
||||
list_of.equations._eqn_3 : ∀ (a : string), list_of (term.cnst a) = list.nil
|
||||
|
|
@ -1,41 +0,0 @@
|
|||
open nat
|
||||
open tactic
|
||||
|
||||
meta def match_le (e : expr) : tactic (expr × expr) :=
|
||||
match expr.is_le e with
|
||||
| (some r) := return r
|
||||
| none := tactic.fail "expression is not a leq"
|
||||
end
|
||||
|
||||
meta def nat_lit_le : tactic unit := do
|
||||
(base_e, bound_e) ← tactic.target >>= match_le,
|
||||
base ← tactic.eval_expr ℕ base_e,
|
||||
skip
|
||||
|
||||
example : 17 ≤ 555555 :=
|
||||
begin
|
||||
nat_lit_le,
|
||||
admit
|
||||
end
|
||||
|
||||
example : { k : ℕ // k ≤ 555555 } :=
|
||||
begin
|
||||
refine subtype.mk _ _,
|
||||
exact 17,
|
||||
target >>= trace,
|
||||
trace_state,
|
||||
nat_lit_le,
|
||||
admit
|
||||
end
|
||||
|
||||
set_option pp.instantiate_mvars false
|
||||
|
||||
example : { k : ℕ // k ≤ 555555 } :=
|
||||
begin
|
||||
refine subtype.mk _ _,
|
||||
exact 17,
|
||||
target >>= trace,
|
||||
trace_state,
|
||||
nat_lit_le,
|
||||
admit
|
||||
end
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
1369.lean:15:0: warning: declaration '[anonymous]' uses sorry
|
||||
17 ≤ 555555
|
||||
⊢ 17 ≤ 555555
|
||||
1369.lean:21:0: warning: declaration '[anonymous]' uses sorry
|
||||
?m_1 ≤ 555555
|
||||
⊢ ?m_1 ≤ 555555
|
||||
1369.lean:33:0: warning: declaration '[anonymous]' uses sorry
|
||||
|
|
@ -1,43 +0,0 @@
|
|||
constants f g h : ℕ → ℕ
|
||||
axiom H_f_g : ∀ n, f (g n) = n
|
||||
|
||||
example (m : ℕ) : h m = h m :=
|
||||
begin
|
||||
let n : ℕ := g m,
|
||||
have H : f n = m := begin rw H_f_g end,
|
||||
subst H, -- Error here
|
||||
end
|
||||
|
||||
set_option pp.instantiate_mvars false
|
||||
|
||||
example (m : ℕ) : h m = h m :=
|
||||
begin
|
||||
let n : ℕ, -- add metavar
|
||||
exact g m,
|
||||
have H : f n = m := begin rw H_f_g end,
|
||||
subst H, -- Error here
|
||||
end
|
||||
|
||||
example (m : ℕ) : h m = h m :=
|
||||
begin
|
||||
let n : ℕ := g m,
|
||||
have H : f n = m := begin rw H_f_g end,
|
||||
subst m, -- Error here
|
||||
end
|
||||
|
||||
set_option pp.instantiate_mvars false
|
||||
|
||||
example (m : ℕ) : h m = h m :=
|
||||
begin
|
||||
let n : ℕ, -- add metavar
|
||||
exact g m,
|
||||
have H : f n = m := begin rw H_f_g end,
|
||||
subst m, -- Error here
|
||||
end
|
||||
|
||||
example (m p: ℕ) : h m = h m :=
|
||||
begin
|
||||
let a : ℕ := g p,
|
||||
let n : ℕ := g a,
|
||||
clear p -- Error here
|
||||
end
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
1467.lean:8:0: error: subst tactic failed, hypothesis 'H' is not of the form (x = t) or (t = x)
|
||||
state:
|
||||
m : ℕ,
|
||||
n : ℕ := g m,
|
||||
H : f n = m
|
||||
⊢ h m = h m
|
||||
1467.lean:18:0: error: subst tactic failed, hypothesis 'H' is not of the form (x = t) or (t = x)
|
||||
state:
|
||||
m : ℕ,
|
||||
n : ℕ := ?m_1,
|
||||
H : f n = m
|
||||
⊢ h m = h m
|
||||
1467.lean:25:0: error: subst tactic failed, hypothesis 'm' is not a variable nor an equation of the form (x = t) or (t = x)
|
||||
state:
|
||||
m : ℕ,
|
||||
n : ℕ := g m,
|
||||
H : f n = m
|
||||
⊢ h m = h m
|
||||
1467.lean:35:0: error: subst tactic failed, hypothesis 'm' is not a variable nor an equation of the form (x = t) or (t = x)
|
||||
state:
|
||||
m : ℕ,
|
||||
n : ℕ := ?m_1,
|
||||
H : f n = m
|
||||
⊢ h m = h m
|
||||
1467.lean:42:0: error: clear tactic failed, hypothesis 'a' depends on 'p'
|
||||
state:
|
||||
m p : ℕ,
|
||||
a : ℕ := g p,
|
||||
n : ℕ := g a
|
||||
⊢ h m = h m
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
def ex (α : Sort _) (a b : α) : a = b :=
|
||||
begin [smt]
|
||||
close -- Should fail
|
||||
end
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
1487.lean:3:2: error: smt_tactic.close failed
|
||||
state:
|
||||
α : Sort ?,
|
||||
a b : α
|
||||
⊢ a = b
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
example (n : ℕ) (h : n = 0) : n = 0 :=
|
||||
by rename n m
|
||||
|
||||
example (n : ℕ) : let x := 10 in n > 0 → x > 5 → n ≠ x → x + 1 = 1 + x :=
|
||||
begin
|
||||
intros,
|
||||
rename x y
|
||||
end
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
1513.lean:2:3: error: tactic failed, there are unsolved goals
|
||||
state:
|
||||
m : ℕ,
|
||||
h : m = 0
|
||||
⊢ m = 0
|
||||
1513.lean:8:0: error: tactic failed, there are unsolved goals
|
||||
state:
|
||||
n : ℕ,
|
||||
a : n > 0,
|
||||
y : ℕ := 10,
|
||||
a_1 : y > 5,
|
||||
a_2 : n ≠ y
|
||||
⊢ y + 1 = 1 + y
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
lemma notc : exists b, b = false :=
|
||||
begin
|
||||
existsi 0, -- ERROR here
|
||||
end
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
1598.lean:3:3: error: existsi tactic failed, type mismatch between given term witness and expected type
|
||||
state:
|
||||
⊢ 0 = false
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
def some_lets : ℕ → ℕ → ℕ
|
||||
| 0 v := v
|
||||
| (nat.succ n) v := let k := some_lets n v + v in k
|
||||
|
||||
def some_unfolded_lets (n : ℕ) : ∃ v : ℕ , v = some_lets 5 n :=
|
||||
begin
|
||||
dunfold some_lets,
|
||||
-- admit
|
||||
end
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
1603.lean:9:0: error: tactic failed, there are unsolved goals
|
||||
state:
|
||||
n : ℕ
|
||||
⊢ ∃ (v : ℕ),
|
||||
v =
|
||||
let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := (let k : ℕ := (let k : ℕ := n + n in k) + n in k) + n in k) + n in k) +
|
||||
n
|
||||
in k
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
meta def mk_cycle : tactic unit :=
|
||||
do [g] <- tactic.get_goals,
|
||||
tactic.refine (pexpr.of_expr g)
|
||||
|
||||
example : true :=
|
||||
by mk_cycle
|
||||
|
||||
meta def mk_cycle2 : tactic unit :=
|
||||
do [g] <- tactic.get_goals,
|
||||
tactic.exact g
|
||||
|
||||
example : true :=
|
||||
by mk_cycle2
|
||||
|
||||
meta def mk_cycle3 : tactic unit :=
|
||||
do [g] <- tactic.get_goals,
|
||||
tactic.refine ``(id %%g)
|
||||
|
||||
example : true :=
|
||||
by mk_cycle3
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
1638.lean:6:3: error: invalid exact tactic, trying to solve goal using itself
|
||||
state:
|
||||
2 goals
|
||||
⊢ true
|
||||
|
||||
⊢ true
|
||||
1638.lean:13:3: error: invalid exact tactic, trying to solve goal using itself
|
||||
state:
|
||||
⊢ true
|
||||
1638.lean:20:3: error: exact tactic failed, failed to assign
|
||||
id ?m_1
|
||||
to metavariable ?m_1 (possible cause: occurs check failed)
|
||||
state:
|
||||
2 goals
|
||||
⊢ true
|
||||
|
||||
⊢ true
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
def some_lets : ℕ → ℕ → ℕ
|
||||
| 0 v := v
|
||||
| (nat.succ n) v := let k := some_lets n v + some_lets n v in some_lets n k
|
||||
|
||||
def some_unfolded_lets (n : ℕ) : Σ' v : ℕ , v = some_lets 5 n :=
|
||||
begin
|
||||
econstructor; dunfold some_lets; econstructor
|
||||
end
|
||||
|
||||
meta def foo : tactic unit :=
|
||||
do [g] <- tactic.get_goals,
|
||||
tactic.to_expr (``(1)) >>= tactic.unify g
|
||||
def some_lifted_lets (n : ℕ) : Σ' (v : ℕ), v = psigma.fst (some_unfolded_lets n) :=
|
||||
begin
|
||||
econstructor; dunfold some_unfolded_lets psigma.fst; symmetry; transitivity; symmetry;
|
||||
{
|
||||
foo -- unify_reify_rhs_to_let_in
|
||||
}
|
||||
|
||||
end
|
||||
|
|
@ -1,176 +0,0 @@
|
|||
1639.lean:17:4: error: unify tactic failed, failed to unify
|
||||
?m_1
|
||||
: ?m_2 =
|
||||
let k : ℕ :=
|
||||
(let k : ℕ :=
|
||||
(let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ :=
|
||||
(let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ :=
|
||||
(let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k
|
||||
and
|
||||
1 : ℕ
|
||||
state:
|
||||
n : ℕ
|
||||
⊢ ?m_1 =
|
||||
let k : ℕ :=
|
||||
(let k : ℕ :=
|
||||
(let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ :=
|
||||
(let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ :=
|
||||
(let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k) +
|
||||
let k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ :=
|
||||
(let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) +
|
||||
let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k,
|
||||
k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k,
|
||||
k : ℕ := k + k
|
||||
in k
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
def f : ℕ → ℕ
|
||||
| a := f a
|
||||
using_well_founded ⟨{0}, well_founded_tactics.default_dec_tac⟩
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
1669.lean:3:20: error: failed to synthesize type class instance for
|
||||
⊢ has_emptyc (expr → list expr → tactic unit)
|
||||
1669.lean:3:20: error: failed to synthesize type class instance for
|
||||
⊢ has_insert ?m_1 (expr → list expr → tactic unit)
|
||||
1669.lean:1:4: error: failed to create auxiliary definition
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
#reduce int.shiftl (-1) (-1)
|
||||
#eval int.shiftl (-1) (-1)
|
||||
|
||||
#reduce int.shiftl (-4) (-2)
|
||||
#eval int.shiftl (-4) (-2)
|
||||
|
||||
#reduce int.shiftl (-5) (-2)
|
||||
#eval int.shiftl (-5) (-2)
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
-[1+ 0]
|
||||
-1
|
||||
-[1+ 0]
|
||||
-1
|
||||
-[1+ 1]
|
||||
-2
|
||||
|
|
@ -1 +0,0 @@
|
|||
def foo: list nat := [ 1,2, ]
|
||||
|
|
@ -1,2 +0,0 @@
|
|||
1745.lean:1:28: error: invalid expression
|
||||
1745.lean:1:0: warning: declaration 'foo' uses sorry
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
section
|
||||
parameter big_type : Type 1
|
||||
parameter x : big_type
|
||||
parameter f {A : Type} : A → bool
|
||||
|
||||
def foo : bool := f x
|
||||
end
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
1760.lean:6:18: error: type mismatch at application
|
||||
f x
|
||||
term
|
||||
x
|
||||
has type
|
||||
big_type : Type 1
|
||||
but is expected to have type
|
||||
?m_1 : Type
|
||||
|
|
@ -1,32 +0,0 @@
|
|||
inductive is_some (x : option nat) : Prop
|
||||
| mk : ∀ value : nat, x = some value → is_some
|
||||
|
||||
def value_1 (x : option nat) (H : is_some x)
|
||||
: nat :=
|
||||
begin
|
||||
destruct x; intros,
|
||||
{destruct H, -- ERROR: `is_some` can only eliminate into Prop
|
||||
intros, clear a_2, rw a at a_1, contradiction},
|
||||
{assumption}
|
||||
end
|
||||
|
||||
def value_2 (x : option nat) (H : is_some x)
|
||||
: x = x :=
|
||||
begin
|
||||
destruct x; intros,
|
||||
{destruct H,
|
||||
intros, rw a at a_1},
|
||||
{refl}
|
||||
end
|
||||
|
||||
inductive is_some' (x : option nat) : Type
|
||||
| mk : ∀ value : nat, x = some value → is_some'
|
||||
|
||||
def value_3 (x : option nat) (H : is_some' x)
|
||||
: nat :=
|
||||
begin
|
||||
destruct x; intros,
|
||||
{destruct H,
|
||||
intros, clear a_2, rw a at a_1, contradiction},
|
||||
{assumption}
|
||||
end
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
1766.lean:8:4: error: destruct tactic failed, recursor 'is_some.cases_on' can only eliminate into Prop
|
||||
state:
|
||||
x : option ℕ,
|
||||
H : is_some x,
|
||||
a : x = none
|
||||
⊢ ℕ
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
theorem nil_subset : (true ∧ true) = true := by simp
|
||||
open list
|
||||
|
||||
example (x : ℕ) : x = x := by simp [nil_subset]
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
1786.lean:4:30: error: ambiguous overload, possible interpretations
|
||||
nil_subset
|
||||
list.nil_subset
|
||||
state:
|
||||
x : ℕ
|
||||
⊢ x = x
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
inductive test : nat -> list nat -> Prop
|
||||
| zero: test 0 list.nil
|
||||
--n remains even
|
||||
| nil: forall {n: nat}, test n list.nil -> test (n+2) list.nil
|
||||
--n flips between even and odd
|
||||
| cons: forall {n i: nat} {is: list nat}, test n is -> test (n+3) (list.cons i is)
|
||||
|
||||
lemma example3 : forall (n m: nat), test (n+n) [m] -> false :=
|
||||
begin
|
||||
intros n m,
|
||||
generalize def_n' : n + n = n',
|
||||
generalize def_is : [m] = is,
|
||||
intro h,
|
||||
revert def_n' def_is,
|
||||
cases h; try {intros, contradiction}, -- smart unfolding prevents the generation of unwieldy terms,
|
||||
trace_state,
|
||||
have : nat.succ (nat.add h_n (nat.add 2 0)) = h_n + 3, from rfl,
|
||||
simp [this], intro h_1,
|
||||
have : n + n = h_n + 3 → false, from sorry,
|
||||
intros,
|
||||
exact this h_1,
|
||||
end
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
case test.cons
|
||||
n m h_n h_i : ℕ,
|
||||
h_is : list ℕ,
|
||||
h_a : test h_n h_is,
|
||||
h : test (nat.succ (nat.add h_n (nat.add 2 0))) (h_i :: h_is)
|
||||
⊢ n + n = nat.succ (nat.add h_n (nat.add 2 0)) → [m] = h_i :: h_is → false
|
||||
1794.lean:8:0: warning: declaration 'example3' uses sorry
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
example : ∀ (p q : Prop), p → q → p :=
|
||||
begin
|
||||
intros p p h1 h2,
|
||||
exact h2,
|
||||
end
|
||||
|
||||
example : ∀ (p q : Prop), p → q → p :=
|
||||
begin
|
||||
intros p p h1 h2,
|
||||
dedup,
|
||||
exact h2,
|
||||
end
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
1814.lean:4:8: error: invalid type ascription, term has type
|
||||
p
|
||||
but is expected to have type
|
||||
p
|
||||
types contain aliased name(s): p
|
||||
remark: the tactic `dedup` can be used to rename aliases
|
||||
state:
|
||||
p p : Prop,
|
||||
h1 : p,
|
||||
h2 : p
|
||||
⊢ p
|
||||
1814.lean:11:8: error: invalid type ascription, term has type
|
||||
p_1
|
||||
but is expected to have type
|
||||
p
|
||||
state:
|
||||
p p_1 : Prop,
|
||||
h1 : p,
|
||||
h2 : p_1
|
||||
⊢ p
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
def f : int → int := λ _, 0
|
||||
|
||||
#check int.add (-1) 1
|
||||
|
||||
#check (-1 : int)
|
||||
|
||||
#check 2 + (-1 : int)
|
||||
|
||||
#check (2 + -1 : int)
|
||||
|
||||
#check f (-1)
|
||||
|
||||
#check 2 * (-1 : int)
|
||||
|
||||
#check (2 * -1 : int)
|
||||
|
||||
#check f 1 < -2
|
||||
|
||||
#check (- - 2 : int)
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
int.add (-1) 1 : ℤ
|
||||
-1 : ℤ
|
||||
2 + -1 : ℤ
|
||||
2 + -1 : ℤ
|
||||
f (-1) : ℤ
|
||||
2 * -1 : ℤ
|
||||
2 * -1 : ℤ
|
||||
f 1 < -2 : Prop
|
||||
- -2 : ℤ
|
||||
|
|
@ -1,21 +0,0 @@
|
|||
structure pType :=
|
||||
(carrier : Type)
|
||||
(Point : carrier)
|
||||
|
||||
structure pmap (A B : pType) : Type :=
|
||||
(f : A.carrier → B.carrier)
|
||||
(p : f A.Point = B.Point)
|
||||
|
||||
def ex1 {A B : pType} (f : pmap A B) : f = f :=
|
||||
begin
|
||||
induction B with B b, induction f with f pf,
|
||||
cases pf -- should fail because of dependency
|
||||
end
|
||||
|
||||
def ex2 {A B : pType} (f : pmap A B) : f = f :=
|
||||
begin
|
||||
induction B with B b, induction f with f pf,
|
||||
dsimp at f, /- break dependency using reduction -/
|
||||
cases pf,
|
||||
refl
|
||||
end
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
1836.lean:12:2: error: cases tactic failed, when eliminating equality right-hand-side depends on left-hand-side
|
||||
state:
|
||||
A : pType,
|
||||
B : Type,
|
||||
b : B,
|
||||
f : A.carrier → {carrier := B, Point := b}.carrier,
|
||||
pf : f (A.Point) = {carrier := B, Point := b}.Point
|
||||
⊢ b = f (A.Point) → pf == _ → {f := f, p := pf} = {f := f, p := pf}
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
prelude
|
||||
class T1 (α : Type) := (O : Type)
|
||||
class T2 (α : Type) extends T1 α
|
||||
class T3 (α : Type) extends T1 α
|
||||
class A (α : Type) [T1 α] := (x : T1.O α)
|
||||
class B (α : Type) [T3 α] extends A α
|
||||
def X {α : Type} [T2 α] : A α := sorry
|
||||
example {α : Type} [T3 α] : B α := { X with }
|
||||
|
|
@ -1,7 +0,0 @@
|
|||
1859.lean:7:0: warning: declaration 'X' uses sorry
|
||||
1859.lean:8:35: error: type mismatch at field 'x'
|
||||
A.x ?m_1
|
||||
has type
|
||||
T1.O ?m_1
|
||||
but is expected to have type
|
||||
T1.O α
|
||||
|
|
@ -1 +0,0 @@
|
|||
run_cmd tactic.trace $ let let_val := (2 : ℕ) in `(id let_val)
|
||||
|
|
@ -1 +0,0 @@
|
|||
id 2
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
def int' := int
|
||||
|
||||
#eval id_rhs int' (-1 : ℤ)
|
||||
-- #2147483647
|
||||
|
||||
instance : has_repr int' :=
|
||||
by unfold int'; apply_instance
|
||||
|
||||
#eval id_rhs int' (-1 : ℤ)
|
||||
-- -1
|
||||
|
||||
@[reducible] def int'' := int
|
||||
|
||||
/- Don't need to define has_repr instance for int'' because it is reducible -/
|
||||
#eval id_rhs int'' (-1 : ℤ)
|
||||
-- -1
|
||||
|
||||
inductive foo
|
||||
| mk₁ : bool → foo
|
||||
| mk₂ : bool → foo
|
||||
|
||||
#eval foo.mk₁ tt
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
1861.lean:3:0: warning: result type does not have an instance of type class 'has_repr', dumping internal representation
|
||||
#2147483647
|
||||
-1
|
||||
-1
|
||||
1861.lean:22:0: warning: result type does not have an instance of type class 'has_repr', dumping internal representation
|
||||
(#0 #1)
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
variable R : Type
|
||||
variable [ring R]
|
||||
|
||||
example : -(-(1:R)) = 1 :=
|
||||
begin
|
||||
trace_state,
|
||||
exact neg_neg 1,
|
||||
end
|
||||
|
||||
#check - -(1:R)
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
R : Type,
|
||||
_inst_1 : ring R
|
||||
⊢ - -1 = 1
|
||||
- -1 : R
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
structure T := (x y : nat)
|
||||
example : T := by refine { x := 1, y := _}
|
||||
example : T := by refine { x := 1, ..}
|
||||
example : T := { x := 1, ..}
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
1870.lean:2:18: error: tactic failed, there are unsolved goals
|
||||
state:
|
||||
⊢ ℕ
|
||||
1870.lean:3:18: error: tactic failed, there are unsolved goals
|
||||
state:
|
||||
⊢ ℕ
|
||||
1870.lean:4:15: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
⊢ ℕ
|
||||
|
|
@ -1 +0,0 @@
|
|||
def X (R : Type) [H : comm_ring R] := H.0
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
1898.lean:1:39: error: invalid projection, index must be greater than 0
|
||||
1898.lean:1:4: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
R : Type,
|
||||
H : comm_ring R
|
||||
⊢ Sort ?
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
def foo : ℕ → false
|
||||
| x :=
|
||||
match x with
|
||||
y := let z := y in foo z /- should fail -/
|
||||
end
|
||||
|
||||
meta def foo2 : ℕ → false
|
||||
| x :=
|
||||
match x with
|
||||
y := let z := y in foo2 z /- should work -/
|
||||
end
|
||||
|
||||
def boo : ℕ → ℕ → bool
|
||||
| 0 m := ff
|
||||
| (n + 1) m :=
|
||||
match m with
|
||||
o := let z := n in boo n (m+1)
|
||||
end
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
1917.lean:4:21: error: failed to prove recursive application is decreasing, well founded relation
|
||||
@has_well_founded.r ℕ (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)
|
||||
Possible solutions:
|
||||
- Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
|
||||
- The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
|
||||
The nested exception contains the failure state for the decreasing tactic.
|
||||
nested exception message:
|
||||
failed
|
||||
state:
|
||||
foo : ℕ → false,
|
||||
x y : ℕ
|
||||
⊢ y < x
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
set_option pp.implicit true
|
||||
|
||||
structure C :=
|
||||
( d : Π { X : Type }, list X → list X )
|
||||
|
||||
def P(c : C):= c.d [0]
|
||||
|
||||
#print P
|
||||
|
|
@ -1,2 +0,0 @@
|
|||
def P : C → list ℕ :=
|
||||
λ (c : C), @C.d c ℕ [0]
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
structure S := (f : ℕ)
|
||||
|
||||
def F : S := { f := prod.1 }
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
1930.lean:3:24: error: invalid field notation, type is not of the form (C ...) where C is a constant
|
||||
prod
|
||||
has type
|
||||
Type ? → Type ? → Type (max ? ?)
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
structure foo :=
|
||||
(fn : nat → nat)
|
||||
(fn_ax : ∀ a : nat, fn a = a)
|
||||
|
||||
/-
|
||||
set_option pp.all true
|
||||
set_option pp.universes false -- universes are probably irrelevant
|
||||
set_option pp.purify_metavars false
|
||||
set_option trace.type_context.is_def_eq true
|
||||
set_option trace.type_context.is_def_eq_detail true
|
||||
-/
|
||||
|
||||
def bla : foo := { fn_ax := λ x, rfl }
|
||||
|
||||
|
||||
instance foo2 (α : Type) : group α := { mul_assoc := λ x y z, rfl }
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
1952.lean:13:17: error: invalid structure value { ... }, field 'fn' was not provided
|
||||
1952.lean:13:28: error: type mismatch at field 'fn_ax'
|
||||
λ (x : ℕ), rfl
|
||||
has type
|
||||
∀ (x : ℕ), ?m_2[x] = ?m_2[x]
|
||||
but is expected to have type
|
||||
∀ (a : ℕ), ⁇ a = a
|
||||
1952.lean:16:38: error: invalid structure value { ... }, field 'mul' was not provided
|
||||
1952.lean:16:38: error: invalid structure value { ... }, field 'one' was not provided
|
||||
1952.lean:16:38: error: invalid structure value { ... }, field 'one_mul' was not provided
|
||||
1952.lean:16:38: error: invalid structure value { ... }, field 'mul_one' was not provided
|
||||
1952.lean:16:38: error: invalid structure value { ... }, field 'inv' was not provided
|
||||
1952.lean:16:38: error: invalid structure value { ... }, field 'mul_left_inv' was not provided
|
||||
1952.lean:16:53: error: type mismatch at field 'mul_assoc'
|
||||
λ (x y z : α), rfl
|
||||
has type
|
||||
∀ (x y z : α), ?m_2[x, y, z] = ?m_2[x, y, z]
|
||||
but is expected to have type
|
||||
∀ (a b c : α), a * b * c = a * (b * c)
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
structure presheaf_of_types (α : Type*) :=
|
||||
(F : Π U : set α, Type*)
|
||||
(res : ∀ (U V : set α) ,
|
||||
(F U) → (F V))
|
||||
(Hidem : ∀ U : set α, res U U = (res U U) ∘ (res U U))
|
||||
|
||||
-- set_option trace.type_context.is_def_eq true
|
||||
-- set_option trace.type_context.is_def_eq_detail true
|
||||
|
||||
definition presheaf_of_types_pushforward
|
||||
{β : Type*}
|
||||
: presheaf_of_types β :=
|
||||
{ Hidem := λ U, rfl,
|
||||
}
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
1952b.lean:13:2: error: invalid structure value { ... }, field 'F' was not provided
|
||||
1952b.lean:13:2: error: invalid structure value { ... }, field 'res' was not provided
|
||||
1952b.lean:13:13: error: type mismatch at field 'Hidem'
|
||||
λ (U : set β), rfl
|
||||
has type
|
||||
∀ (U : set β), ?m_2[U] = ?m_2[U]
|
||||
but is expected to have type
|
||||
∀ (U : set β), ⁇ U U = ⁇ U U ∘ ⁇ U U
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
universe variables u
|
||||
variables (A : Type u) [H : inhabited A] (x : A)
|
||||
include H
|
||||
|
||||
definition foo := x
|
||||
#check foo -- A and x are explicit
|
||||
|
||||
variables {A x}
|
||||
definition foo' := x
|
||||
#check @foo' -- A is explicit, x is implicit
|
||||
|
||||
open nat
|
||||
|
||||
#check foo nat 10
|
||||
|
||||
definition test : @foo' ℕ _ 10 = (10:nat) := rfl
|
||||
|
||||
set_option pp.implicit true
|
||||
#print test
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
foo : Π (A : Type u_1) [H : inhabited A], A → A
|
||||
foo' : Π {A : Type u_1} [H : inhabited A] {x : A}, A
|
||||
foo ℕ 10 : ℕ
|
||||
def test : ∀ {A : Type u} [H : inhabited A], @foo' ℕ nat.inhabited (5 + 5) = 10 :=
|
||||
λ {A : Type u} [H : inhabited A], @rfl ℕ (@foo' ℕ nat.inhabited (5 + 5))
|
||||
|
|
@ -1,27 +0,0 @@
|
|||
section
|
||||
universe variable u variable (A : Type u)
|
||||
|
||||
section
|
||||
variables (a b : A)
|
||||
variable (H : a = b)
|
||||
|
||||
definition tst₁ := a
|
||||
|
||||
#check @tst₁
|
||||
|
||||
variable {A}
|
||||
|
||||
definition tst₂ := a
|
||||
|
||||
#check @tst₂ -- A is implicit
|
||||
|
||||
lemma symm₂ : b = a := eq.symm H
|
||||
|
||||
#check @symm₂
|
||||
end
|
||||
|
||||
variable (a : A)
|
||||
definition tst₃ := a
|
||||
|
||||
#check @tst₃ -- A is explicit again
|
||||
end
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
tst₁ : Π (A : Type u_1), A → A
|
||||
tst₂ : Π {A : Type u_1}, A → A
|
||||
symm₂ : ∀ {A : Type u_1} (a b : A), a = b → b = a
|
||||
tst₃ : Π (A : Type u_1), A → A
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
section
|
||||
universe variables u parameter (A : Type u)
|
||||
|
||||
section
|
||||
parameters (a b : A)
|
||||
parameter (H : a = b)
|
||||
|
||||
definition tst₁ := a
|
||||
|
||||
parameter {A}
|
||||
|
||||
definition tst₂ := a
|
||||
|
||||
lemma symm₂ : b = a := eq.symm H
|
||||
|
||||
parameters {a b}
|
||||
lemma foo (c : A) (h₂ : c = b) : c = a :=
|
||||
eq.trans h₂ symm₂
|
||||
end
|
||||
|
||||
parameter (a : A)
|
||||
definition tst₃ := a
|
||||
end
|
||||
|
||||
#check @tst₁
|
||||
#check @tst₂ -- A is implicit
|
||||
#check @symm₂
|
||||
#check @tst₃ -- A is explicit again
|
||||
#check @foo
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
tst₁ : Π (A : Type u_1), A → A
|
||||
tst₂ : Π {A : Type u_1}, A → A
|
||||
symm₂ : ∀ {A : Type u_1} (a b : A), a = b → b = a
|
||||
tst₃ : Π (A : Type u_1), A → A
|
||||
foo : ∀ {A : Type u_1} {a b : A}, a = b → ∀ (c : A), c = b → c = a
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
open nat
|
||||
namespace foo
|
||||
section
|
||||
parameter (X : Type)
|
||||
definition A {n : ℕ} : Type := X
|
||||
variable {n : ℕ}
|
||||
set_option pp.implicit true
|
||||
#check @A n
|
||||
set_option pp.full_names true
|
||||
#check @foo.A n
|
||||
#check @A n
|
||||
|
||||
set_option pp.full_names false
|
||||
#check @foo.A n
|
||||
#check @A n
|
||||
end
|
||||
end foo
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
@A n : Type
|
||||
@foo.A n : Type
|
||||
@foo.A n : Type
|
||||
@A n : Type
|
||||
@A n : Type
|
||||
|
|
@ -1,41 +0,0 @@
|
|||
open nat
|
||||
namespace foo
|
||||
section
|
||||
parameter (X : Type)
|
||||
definition A {n : ℕ} : Type := X
|
||||
definition B : Type := X
|
||||
variable {n : ℕ}
|
||||
#check @A n
|
||||
#check foo.A
|
||||
#check foo.A
|
||||
#check @foo.A 10
|
||||
#check @foo.A n
|
||||
#check @foo.A n
|
||||
#check @foo.A n
|
||||
|
||||
set_option pp.full_names true
|
||||
#check A
|
||||
#check foo.A
|
||||
#check @foo.A 10
|
||||
#check @foo.A n
|
||||
#check @foo.A n
|
||||
|
||||
set_option pp.full_names false
|
||||
|
||||
set_option pp.implicit true
|
||||
#check @A n
|
||||
#check @foo.A 10
|
||||
#check @foo.A n
|
||||
set_option pp.full_names true
|
||||
#check @foo.A n
|
||||
#check @A n
|
||||
|
||||
set_option pp.full_names false
|
||||
#check @foo.A n
|
||||
#check @foo.A n
|
||||
#check @foo.A n
|
||||
#check @foo.A n
|
||||
#check @foo.A n
|
||||
#check @A n
|
||||
end
|
||||
end foo
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
A : Type
|
||||
A : Type
|
||||
A : Type
|
||||
A : Type
|
||||
A : Type
|
||||
A : Type
|
||||
A : Type
|
||||
foo.A : Type
|
||||
foo.A : Type
|
||||
foo.A : Type
|
||||
foo.A : Type
|
||||
foo.A : Type
|
||||
@A n : Type
|
||||
@A 10 : Type
|
||||
@A n : Type
|
||||
@foo.A n : Type
|
||||
@foo.A n : Type
|
||||
@A n : Type
|
||||
@A n : Type
|
||||
@A n : Type
|
||||
@A n : Type
|
||||
@A n : Type
|
||||
@A n : Type
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
open nat
|
||||
section
|
||||
parameter (X : Type)
|
||||
definition A {n : ℕ} : Type := X
|
||||
definition B : Type := X
|
||||
variable {n : ℕ}
|
||||
#check @A n
|
||||
#check _root_.A nat
|
||||
#check _root_.A (X × B)
|
||||
#check @_root_.A (X × B) 10
|
||||
#check @_root_.A (_root_.B (@_root_.A X n)) n
|
||||
#check @_root_.A (@_root_.B (@_root_.A nat n)) n
|
||||
|
||||
set_option pp.full_names true
|
||||
#check A
|
||||
#check _root_.A nat
|
||||
#check @_root_.A (X × B) 10
|
||||
#check @_root_.A (@_root_.B (@_root_.A X n)) n
|
||||
#check @_root_.A (@_root_.B (@_root_.A nat n)) n
|
||||
|
||||
set_option pp.full_names false
|
||||
|
||||
set_option pp.implicit true
|
||||
#check @A n
|
||||
#check @_root_.A nat 10
|
||||
#check @_root_.A X n
|
||||
set_option pp.full_names true
|
||||
#check @_root_.A X n
|
||||
#check @_root_.A B n
|
||||
|
||||
set_option pp.full_names false
|
||||
#check @_root_.A X n
|
||||
#check @_root_.A B n
|
||||
#check @_root_.A (@_root_.B (@A n)) n
|
||||
#check @_root_.A (@_root_.B (@_root_.A X n)) n
|
||||
#check @_root_.A (@_root_.B (@_root_.A nat n)) n
|
||||
#check @A n
|
||||
end
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
A : Type
|
||||
_root_.A ℕ : Type
|
||||
_root_.A (X × B) : Type
|
||||
_root_.A (X × B) : Type
|
||||
_root_.A (_root_.B A) : Type
|
||||
_root_.A (_root_.B (_root_.A ℕ)) : Type
|
||||
A : Type
|
||||
_root_.A ℕ : Type
|
||||
_root_.A (X × B) : Type
|
||||
_root_.A (_root_.B A) : Type
|
||||
_root_.A (_root_.B (_root_.A ℕ)) : Type
|
||||
@A n : Type
|
||||
@_root_.A ℕ 10 : Type
|
||||
@A n : Type
|
||||
@A n : Type
|
||||
@_root_.A B n : Type
|
||||
@A n : Type
|
||||
@_root_.A B n : Type
|
||||
@_root_.A (_root_.B (@A n)) n : Type
|
||||
@_root_.A (_root_.B (@A n)) n : Type
|
||||
@_root_.A (_root_.B (@_root_.A ℕ n)) n : Type
|
||||
@A n : Type
|
||||
Some files were not shown because too many files have changed in this diff Show more
Loading…
Add table
Reference in a new issue