| import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction | |
| import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading | |
| set_option pp.proofs.withType false | |
| variable {R M} [CommRing R] [Invertible (2 : R)] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) | |
| abbrev ExteriorAlgebra.rMultivector (r : ℕ) : Submodule R (ExteriorAlgebra R M) := | |
| (LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] _) ^ r) |
| /- | |
| This file demonstrates the use of VSCode [Spell Right](https://marketplace.visualstudio.com/items?itemName=ban.spellright) | |
| extension to spell check comments in Lean 4 files while avoiding code or code blocks in comments, it uses some heuristics | |
| to work for both Markdown and [reStructuredText](https://devguide.python.org/documentation/markup/) per request on | |
| [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Spell.20check). | |
| The minimal configuration to make it work for Lean is to add the following to your `settings.json` after the installing | |
| the extension, setting up [the spell check dictionaries](https://github.com/bartosz-antosik/vscode-spellright#dictionaries), | |
| and [enable spell check for the language of your choosing](https://github.com/bartosz-antosik/vscode-spellright#changing-language-and-turning-off): |
| /* | |
| You may use it via https://github.com/openstyles/stylus/ , matching url prefix: https://live.lean-lang.org/ | |
| */ | |
| /* | |
| Code for dark style of the Monaco editor |
This guide might be of use when you are in a situation where you know exactly what you want to do "in real life" in your proof, but don't know how to do it in Lean. For example, you might be faced with a hypothesis of the form p ∧ q and you need a proof of p, or you might be faced with a goal of the form p ∨ q which you want to deduce from a proof of p.
Let's say that you know your next step involves p ∧ q in some way. Which tactic you use depends on whether p ∧ q is a hypothesis (i.e. you have the assumption H : p ∧ q in your local context) or the goal (i.e. what you are trying to prove). If it is a hypothesis then you need to eliminate it, whereas if it is the goal then you need to introduce it
Once you have established whether you want to introduce or eliminate it, find the function in the list below and you will see the tactic you need. Click on the link to see an example of usage.
| 岩浆 | |
| ---- | |
| 时偿积欠缺填勉， 凝途失涩兴阑珊。 | |
| 奔流方遒黯如没， 趣中汲静思里安。 | |
| 泳夜 | |
| ---- |
| cmake_minimum_required(VERSION 2.8) | |
| macro (show variable value) | |
| message("${variable} = ${value}") | |
| endmacro() | |
| function(join VALUES GLUE OUTPUT) | |
| string (REPLACE ";" "${GLUE}" _TMP_STR "${VALUES}") | |
| set (${OUTPUT} "${_TMP_STR}" PARENT_SCOPE) | |
| endfunction() |
| var shelljs = require('shelljs'); | |
| var fs = require("fs"); | |
| var path = require("path"); | |
| var root = process.argv[2]; | |
| if(!root) | |
| { | |
| console.log("root is not specified"); | |
| process.exit(); |
utensilsong@vm-1:~/projects/DavidRagazzi/nupic$ echo $NUPIC
utensilsong@vm-1:~/projects/DavidRagazzi/nupic$ echo $NTA
utensilsong@vm-1:~/projects/DavidRagazzi/nupic$ export REPOSITORY=`pwd`
utensilsong@vm-1:~/projects/DavidRagazzi/nupic$ mkdir $REPOSITORY/build_system
mkdir: cannot create directory ‘/home/utensilsong/projects/DavidRagazzi/nupic/build_system’: File exists
utensilsong@vm-1:~/projects/DavidRagazzi/nupic$