From 1e5e3152bdfc3018f76ec44271e2446f1102dd7e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dennis=20M=C3=BCller?= <d.mueller@jacobs-university.de>
Date: Sun, 23 Jul 2017 13:54:10 +0100
Subject: [PATCH] Higher-Unicode-Delimiters
---
source/mmt/Quantities.mmt | 105 ++++++-----
source/mmt/VanRoosbroeck.mmt | 22 +--
source/mmt/band.mmt | 36 ++--
source/mmt/constants.mmt | 55 +++---
source/mmt/continuity.mmt | 65 ++++---
source/mmt/densities.mmt | 34 ++--
source/mmt/device.mmt | 90 +++++-----
source/mmt/poisson.mmt | 90 +++++-----
source/mmt/recombination.mmt | 32 ++--
source/mmt/species.mmt | 26 +--
source/thermistor/quantities.mmt | 298 +++++++++++++++----------------
11 files changed, 428 insertions(+), 425 deletions(-)
diff --git a/source/mmt/Quantities.mmt b/source/mmt/Quantities.mmt
index 97b6a73..9d0bb89 100644
--- a/source/mmt/Quantities.mmt
+++ b/source/mmt/Quantities.mmt
@@ -1,70 +1,69 @@
-namespace http://mathhub.info/MitM/Models
-import qe http://mathhub.info/MitM/Foundation/Units
+namespace http://mathhub.info/MitM/Models âš
+import qe http://mathhub.info/MitM/Foundation/Units âš
-/T This is a theory containing the electric displacement.
+/T This is a theory containing the electric displacement. âš
theory Displacement : qe:?SIUnits =
- // meta modeltype physical_quantity
- displacement_dim : type = QE (ElectricCharge /' (Length *' Length))
- displacement : displacement_dim # D
-
+ // meta modeltype physical_quantity â™
+ displacement_dim : dimension ☠= ElectricCharge /' (Length *' Length) â™
+ displacement : QE displacement_dim ☠# D ☠role Quantity â™
+âš
theory Permittivity : qe:?SIUnits =
- // meta modeltype physical_quantity
- permittivity_dim : type = QE (ElectricCharge /' (ElectricPotential *' Length))
- permittivity : permittivity_dim # εs
-
+ // meta modeltype physical_quantity â™
+ permittivity_dim : dimension ☠= ElectricCharge /' (ElectricPotential *' Length) â™
+ permittivity : QE permittivity_dim ☠# ε_s ☠role Quantity â™
+âš
theory Density : qe:?SIUnits =
- // meta modeltype physical_quantity
- density_dim : dimension = (DimNone /' (Length *' Length *' Length))
- density : QE density_dim
-
+ // meta modeltype physical_quantity â™
+ density_dim : dimension ☠= (DimNone /' (Length *' Length *' Length)) â™
+ density : QE density_dim ☠role Quantity ☠# d â™
+âš
theory CurrentDensity : qe:?SIUnits =
- // meta modeltype physical_quantity
- currentdensity_dim : dimension = (Current /' Area)
- currentdensity : QE currentdensity_dim
-
+ // meta modeltype physical_quantity â™
+ currentdensity_dim : dimension ☠= (Current /' Area) â™
+ currentdensity : QE currentdensity_dim ☠role Quantity â™
+âš
-theory RecombinationRate : qe:?QEBase =
- include Models/device?DeviceGeometry
- // meta modeltype physical_quantity
- recombinationrate_dim : dimension = DimNone /' (Volume *' Time)
- recombinationrate : Ω → QE recombinationrate_dim # R
-
+theory RecombinationRate : qe:?SIUnits =
+ include Models/device?DeviceGeometry â™
+ // meta modeltype physical_quantity â™
+ recombinationrate_dim : dimension ☠= DimNone /' (Volume *' Time) â™
+ recombinationrate : Ω → QE recombinationrate_dim ☠# R ☠role Quantity â™
+âš
-theory RecombinationCoefficient : top:?Base =
- include ?Density
- recombination_coefficient : QE density_dim → QE density_dim → QE (Volume /' Time) # r 1 2
+theory RecombinationCoefficient : qe:?SIUnits =
+ include ?Density â™
+ recombination_coefficient : QE density_dim → QE density_dim → QE (Volume /' Time) ☠# r ☠role Quantity â™
+âš
-
-
-theory Energy : qe:?QEBase =
- energy : QE Energy
-
+theory Energy : qe:?SIUnits =
+ energy : QE Energy ☠# E ☠role Quantity â™
+âš
-theory SpatialDensity : qe:?QEBase =
- include Models/device?DeviceGeometry
- include ?Density
- spatialdensity : Ω → QE density_dim # n 1
-
+theory SpatialDensity : qe:?SIUnits =
+ include Models/device?DeviceGeometry â™
+ include ?Density â™
+ spatialdensity : Ω → QE density_dim ☠# n ☠role Quantity â™
+âš
-theory SpatialPotential : top:?Base =
- include Models/device?DeviceGeometry
+theory SpatialPotential : qe:?SIUnits =
+ include Models/device?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- potential : Ω → (QE ElectricPotential) # φ 1
-
+ usually denoted by $φ$. â™
+ potential : Ω → (QE ElectricPotential) ☠# φ ☠role Quantity â™
+âš
-theory SpatialChargeDensity : top:?Base =
- include Models/device?DeviceGeometry
- include ?Density
- charge : Ω → QE (ElectricCharge *' density_dim) # Q 1
-
+theory SpatialChargeDensity : qe:?SIUnits =
+ include Models/device?DeviceGeometry â™
+ include ?Density â™
+ charge : Ω → QE (ElectricCharge *' density_dim) ☠# Q ☠role Quantity â™
+âš
-theory SpatialCurrentDensity : top:?Base =
- include Models/device?DeviceGeometry
- include ?CurrentDensity
- spatialcurrentdensity : Ω → QE currentdensity_dim # j 1
-
\ No newline at end of file
+theory SpatialCurrentDensity : qe:?SIUnits =
+ include Models/device?DeviceGeometry â™
+ include ?CurrentDensity â™
+ spatialcurrentdensity : Ω → QE currentdensity_dim ☠# j ☠role Quantity â™
+âš
\ No newline at end of file
diff --git a/source/mmt/VanRoosbroeck.mmt b/source/mmt/VanRoosbroeck.mmt
index 8e8c6f7..ba4fc58 100644
--- a/source/mmt/VanRoosbroeck.mmt
+++ b/source/mmt/VanRoosbroeck.mmt
@@ -1,5 +1,5 @@
-namespace http://mathhub.info/MitM/Models/VanRoosbroeck
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/VanRoosbroeck âš
+import top http://mathhub.info/MitM/Models âš
/T This is a theory containing the stationary van Roosbroeck system
describung the charge transport of electrons and holes
@@ -11,13 +11,13 @@ import top http://mathhub.info/MitM/Models
density of states, mobilties are assumed to be
homogenous (spatially constant). Also a homogenous device
temperature is assumed.
-
+ âš
theory VanRoosbroeck : top:?Base =
- include poisson?PoissonEquation
- include poisson?PoissonBoundaryConditions
- include continuity?ContinuityEquationElectrons
- include continuity?ContinuityEquationHoles
- include continuity?ContinuityBoundaryConditionsElectrons
- include continuity?ContinuityBoundaryConditionsHoles
- include recombination?SpontaneousRecombination
-
\ No newline at end of file
+ include poisson?PoissonEquation â™
+ include poisson?PoissonBoundaryConditions â™
+ include continuity?ContinuityEquationElectrons â™
+ include continuity?ContinuityEquationHoles â™
+ include continuity?ContinuityBoundaryConditionsElectrons â™
+ include continuity?ContinuityBoundaryConditionsHoles â™
+ include recombination?SpontaneousRecombination â™
+âš
\ No newline at end of file
diff --git a/source/mmt/band.mmt b/source/mmt/band.mmt
index 2a40dde..86ae3d0 100644
--- a/source/mmt/band.mmt
+++ b/source/mmt/band.mmt
@@ -1,24 +1,24 @@
-namespace http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models âš
/T This is a theory containing the bandstructure parameters of
- the semiconductor.
-/T Parameter
-theory BandstructureParameters : top:?Base =
- structure effective_density : top:?Density =
- density @ effective_density_of_states # N
-
+ the semiconductor. âš
+/T Parameter âš
+theory BandstructureParameters : ?Base =
+ structure effective_density : ?Density =
+ density @ effective_density_of_states ☠# N â™
+ âš
/T The effective density of states for the conduction bands
- usually denoted by $N$.
- /T The conduction band edge usually denoted by $E$.
- band_edge : QE Energy # E
- /T Charge number (for electrons -1, for holes 1)
- charge_number : ℤ # z
- mobility : QE (Area /' (ElectricPotential *' Time)) # μ
-
+ usually denoted by $N$. â™
+ /T The conduction band edge usually denoted by $E$. â™
+ band_edge : QE Energy ☠# E â™
+ /T Charge number (for electrons -1, for holes 1) â™
+ charge_number : ℤ ☠# z â™
+ mobility : QE (Area /' (ElectricPotential *' Time)) ☠# μ â™
+âš
theory Band : top:?Base =
- include ?BandstructureParameters
+ include ?BandstructureParameters â™
structure fermi : top:?SpatialPotential =
- potential # φ 1
-
-
\ No newline at end of file
+ potential # φ â™
+ âš
+âš
\ No newline at end of file
diff --git a/source/mmt/constants.mmt b/source/mmt/constants.mmt
index 7001b49..dc989a9 100644
--- a/source/mmt/constants.mmt
+++ b/source/mmt/constants.mmt
@@ -1,31 +1,36 @@
-namespace http://mathhub.info/MitM/Models
-import mitm http://mathhub.info/MitM
-import lfx http://gl.mathhub.info/MMT/LFX
+namespace http://mathhub.info/MitM/Models âš
+import mitm http://mathhub.info/MitM âš
+import lfx http://gl.mathhub.info/MMT/LFX âš
+import rules scala://LFX.mmt.kwarc.info âš
-/T This is a theory containing general physical constants
+/T This is a theory containing general physical constants âš
theory PhysicalConstants : mitm:/Foundation/Units?SIUnits =
- include ?Permittivity
- include mitm:/smglom/arithmetics?realarith
- /T The vaccuum dielectric permitivity constant (usually denoted by $ε_0$)
- vacuum_dielectric_permitivity : permittivity_dim # ε_0
- /T The elementary charge (denoted by $q$)
- elementary_charge : QE ElectricCharge # q
- /T The Boltzmann constant (usually denoted by $k_B$)
- Boltzmann_constant : QE (Energy /' Temperature) # k_B
-
+ include ?Permittivity â™
+ include mitm:/smglom/arithmetics?realarith â™
+ /T The vaccuum dielectric permitivity constant (usually denoted by $ε_0$) â™
+ vacuum_dielectric_permitivity : QE permittivity_dim ☠# ε_0 â™
+ /T The elementary charge (denoted by $q$) â™
+ elementary_charge : QE ElectricCharge ☠# q â™
+ /T The Boltzmann constant (usually denoted by $k_B$) â™
+ Boltzmann_constant : QE (Energy /' Temperature) ☠# k_B â™
+âš
theory Base : mitm:/smglom/arithmetics?realarith =
- include ?PhysicalConstants
- include http://mathhub.info/MitM/smglom/calculus?derivative
- // TODO anständige ableitung (Einheiten!!)
- unit_pred : {D : dimension, P : ℠→ bool} type
- = [D,P] ⟨ QE D | [x] ⊦ P (scalar x) ⟩ # dpred 1 2
- inof : {D : dimension, u : unit D, P : ℠→ bool, r : pred P}dpred D P # 4 inof 2 // TODO
- scalarp : {D : dimension, P : ℠→ bool} dpred D P → pred P # scalarp 3
+ include ?PhysicalConstants â™
+ include http://mathhub.info/MitM/smglom/calculus?derivative â™
+ // TODO anständige ableitung (Einheiten!!) â™
+ unit_pred : {D : dimension, P : ℠→ bool} type â˜
+ = [D,P] ⟨ QE D | [x] ⊦ P (scalar x) ⟩ ☠# dpred 1 2 â™
+ inof : {D : dimension, u : unit D, P : ℠→ bool, r : pred P}dpred D P ☠# 4 inof 2 â™ // TODO â™
+ scalarp : {D : dimension, P : ℠→ bool} dpred D P → pred P ☠# scalarp 3 â™
- // TODO
- // unit_derivative : {P : ℠→ bool, Da : dimension, Db : dimension, u : unit Da, f : (dpred Da P) → QE Db, p : ⊦ diff [x : pred P] scalar (f (x inof u))} dpred Da P → QE Db
- = [P,Da,Db,u,f,p] ([y] ([x : pred P] (scalar (f (x inof u)))' (scalarp y)) of (unitof y) )
+ rule rules?QuantityRule â™
+ rule rules?LawRule â™
+ rule rules?ModelRule â™
- // Ω = kompakte, einfach zusammenhängende teilmenge des â„^n für n â€âˆˆ 4
-
+ // TODO â™
+ // unit_derivative : {P : ℠→ bool, Da : dimension, Db : dimension, u : unit Da, f : (dpred Da P) → QE Db, p : ⊦ diff [x : pred P] scalar (f (x inof u))} dpred Da P → QE Db â˜
+ = [P,Da,Db,u,f,p] ([y] ([x : pred P] (scalar (f (x inof u)))' (scalarp y)) of (unitof y) ) â™
+
+ // Ω = kompakte, einfach zusammenhängende teilmenge des â„^n für n â€âˆˆ 4 â™
+âš
diff --git a/source/mmt/continuity.mmt b/source/mmt/continuity.mmt
index 6ae3c84..c245e76 100644
--- a/source/mmt/continuity.mmt
+++ b/source/mmt/continuity.mmt
@@ -1,60 +1,59 @@
-namespace http://mathhub.info/MitM/Models/continuity
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/continuity âš
+import top http://mathhub.info/MitM/Models âš
/T This is a theory containing the mobilitiy parameters of
- the semiconductor.
+ the semiconductor. âš
theory Mobility : top:?Base =
- /T The mobility parameter usually denoted by $μ$.
-
+ /T The mobility parameter usually denoted by $μ$. â™
+âš
-/T This is a theory containing the expression for the hole current.
+/T This is a theory containing the expression for the hole current. âš
theory CurrentLaw : top:?Base =
- include top:?Band
- include top:?BandstructureParameters
- include top:?SpatialCurrentDensity
+ include top:?Band â™
+ include top:?SpatialCurrentDensity â™
/T Defintion of the hole current in gradient form.
The driving force of the current are the negative gradient of
- the quasi-Fermi potential, here denoted by j_p.
- // TODO: change to more natural formulation later, e.g. f-> xψ, g-> xφ_p?
+ the quasi-Fermi potential, here denoted by j_p. â™
+ // TODO: change to more natural formulation later, e.g. f-> xψ, g-> xφ_p? â™
- current_law : {x : Ω} ⊦ j x ≠-q ⋅ μ ⋅ (n x) ⋅ ((φ ') x)
-
+ current_law : {x : Ω} ⊦ j x ≠-q â‹… μ â‹… (N x) â‹… ((φ ') x) ☠role Law â™
+âš
-/T This is a theory containing the continuity equation for the electrons.
+/T This is a theory containing the continuity equation for the electrons. âš
theory ContinuityEquation : top:?Base =
- include top:/Species?Species
- include top:?RecombinationRate
+ include top:/Species?Species â™
+ include top:?RecombinationRate â™
- /T Formulation of the continuity equation for electrons in divergence form.
+ /T Formulation of the continuity equation for electrons in divergence form. â™
continuity_equation :
- {x : Ω} ⊦ (j ') x ≠-z (R x)
-
+ {x : Ω} ⊦ (j ') x ≠-z (R x) ☠role Law â™
+âš
/T This is a theory containing the boundary conditions for the
- electron continuity equation modeling Ohmic contacts.
+ electron continuity equation modeling Ohmic contacts. âš
theory ContinuityBoundaryConditionsElectrons : top:?Base =
- include device?DeviceOperationState
- /T Boundary condition for the top contact.
- potential_top : QE ElectricPotential = U_1 # φ_n_1
- /T Boundary condition for the bottom contact.
- potential_bottom : QE ElectricPotential = U_2 # φ_n_2
-
+ include device?DeviceOperationState â™
+ /T Boundary condition for the top contact. â™
+ potential_top : QE ElectricPotential ☠= U_1 ☠# φ_n_1 â™
+ /T Boundary condition for the bottom contact. â™
+ potential_bottom : QE ElectricPotential ☠= U_2 ☠# φ_n_2 â™
+âš
/T This is a theory containing the boundary conditions for the
- holes continuity equation modeling Ohmic contacts.
+ holes continuity equation modeling Ohmic contacts. âš
theory ContinuityBoundaryConditionsHoles : top:?Base =
- include device?DeviceOperationState
- /T Boundary condition for the top contact.
- potential_top : QE ElectricPotential = U_1 # φ_p_1
- /T Boundary condition for the bottom contact.
- potential_bottom : QE ElectricPotential = U_2 # φ_p_2
-
\ No newline at end of file
+ include device?DeviceOperationState â™
+ /T Boundary condition for the top contact. â™
+ potential_top : QE ElectricPotential ☠= U_1 ☠# φ_p_1 â™
+ /T Boundary condition for the bottom contact. â™
+ potential_bottom : QE ElectricPotential ☠= U_2 ☠# φ_p_2 â™
+âš
\ No newline at end of file
diff --git a/source/mmt/densities.mmt b/source/mmt/densities.mmt
index af435b1..dfa55f6 100644
--- a/source/mmt/densities.mmt
+++ b/source/mmt/densities.mmt
@@ -1,22 +1,22 @@
-namespace http://mathhub.info/MitM/Models/densities
-import top http://mathhub.info/MitM/Models
-import arith http://mathhub.info/MitM/smglom/arithmetics
+namespace http://mathhub.info/MitM/Models/densities âš
+import top http://mathhub.info/MitM/Models âš
+import arith http://mathhub.info/MitM/smglom/arithmetics âš
/T This is a theory containing state equation for the
- density for the Boltzmann approximation (exp).
-/T Solution
+ density for the Boltzmann approximation (exp). âš
+/T Solution âš
theory DensityLaw : top:?Base =
-// meta model_type physical_law
- include device?DeviceOperationState
- include top:?PhysicalConstants
- include top:?Density
- include top:?SpatialDensity
+// meta model_type physical_law â™
+ include device?DeviceOperationState â™
+ include top:?PhysicalConstants â™
+ include top:?Density â™
+ include top:?SpatialDensity â™
structure electrostatic : top:?SpatialPotential =
- domain = `top:/device?DeviceGeometry?domain
- potential # ψ
- // should be an include, but...
- structure band : top:?Band =
- /T Formula for the electron density for the Boltzmann approximation.
- density_law : {x : Ω} ⊦ n x ≠N ⋅ `arith:?realarith?exponentiation (scalar (((- q) ⋅ z ⋅ ((ψ x) - (φ x)) - E) / k_B ⋅ T))
-
\ No newline at end of file
+ domain = `top:/device?DeviceGeometry?domain â™
+ potential # ψ â™
+ âš // should be an include, but... â™
+ structure band : top:?Band = âš
+ /T Formula for the electron density for the Boltzmann approximation. â™
+ density_law : {x : Ω} ⊦ n x ≠N â‹… `arith:?realarith?exponentiation (scalar (((- q) â‹… z â‹… ((ψ x) - (φ x)) - E) / k_B â‹… T)) ☠role Law â™
+âš
\ No newline at end of file
diff --git a/source/mmt/device.mmt b/source/mmt/device.mmt
index 89c551c..dfb5f88 100644
--- a/source/mmt/device.mmt
+++ b/source/mmt/device.mmt
@@ -1,63 +1,63 @@
-namespace http://mathhub.info/MitM/Models/device
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/device âš
+import top http://mathhub.info/MitM/Models âš
-/T This theory intentionally left empty. It has a narrative in sTeX
-/T Background
-theory Device =
+/T This theory intentionally left empty. It has a narrative in sTeX âš
+/T Background âš
+theory Device = âš
-/T This is a theory containing description of device geometry.
-/T Parameter
+/T This is a theory containing description of device geometry. âš
+/T Parameter âš
theory DeviceGeometry : top:?Base =
- include ?Device
- // domain_prop : â„3 → bool
- domain_prop : ℠→ bool
- /T The one-dimensional spatial domain of the device (denoted by $Ω$).
- // domain : type = pred3 domain_prop # Ω
- domain : type = pred domain_prop # Ω
-
+ include ?Device â™
+ // domain_prop : â„3 → bool â™
+ domain_prop : ℠→ bool â™
+ /T The one-dimensional spatial domain of the device (denoted by $Ω$). â™
+ // domain : type ☠= pred3 domain_prop ☠# Ω â™
+ domain : type ☠= pred domain_prop ☠# Ω â™
+âš
// theory OneDimDeviceGeometry : top:?Base =
- bottom : â„
- top : â„
- Interval_pred : ℠→ bool = [r] bottom ≤ r ∧ r ≤ top
- Omega_Interval : type = pred Interval_pred # I
+ bottom : â„ â™
+ top : â„ â™
+ Interval_pred : ℠→ bool ☠= [r] bottom ≤ r ∧ r ≤ top â™
+ Omega_Interval : type ☠= pred Interval_pred ☠# I â™
structure Geometry : ?DeviceGeometry =
- domain_prop = t1↑ Interval_pred
-
-//
+ domain_prop = t1↑ Interval_pred â™
+ âš
+// âš
// theory TwoDimDeviceGeometry : top:?Base =
- Plane_pred : â„2 → bool
- Omega_Plane : type = pred2 Plane_pred # G
+ Plane_pred : â„2 → bool â™
+ Omega_Plane : type ☠= pred2 Plane_pred ☠# G â™
structure Geometry : ?DeviceGeometry =
- domain_prop = t2↑ Plane_pred
-
-//
+ domain_prop = t2↑ Plane_pred â™
+ âš
+// âš
-/T This is a theory containing description of the doping profile.
-/T Parameter
+/T This is a theory containing description of the doping profile. âš
+/T Parameter âš
theory DopingProfile : top:?Base =
- include ?DeviceGeometry
- include top:?Density
- /T The doping profile, denoted by $C$.
- doping_profile : Ω → QE density_dim # C
-
+ include ?DeviceGeometry â™
+ include top:?Density â™
+ /T The doping profile, denoted by $C$. â™
+ doping_profile : Ω → QE density_dim ☠# C â™
+âš
/T This is a theory containing a description the the operating state,
- that means applied voltages and device temperature.
-/T Parameter
+ that means applied voltages and device temperature. âš
+/T Parameter âš
theory DeviceOperationState : top:?Base =
- include ?DeviceGeometry
- /T The global temperature of the device denoted by $T$.
- // temperature : Ω → ℠# T
- temperature : QE Temperature # T
- /T The applied voltage at the bottom contact denoted by $U_1$.
- voltage_bottom : QE ElectricPotential # U_1
- /T The applied voltage at the top contact denoted by $U_2$.
- voltage_top : QE ElectricPotential # U_2
+ include ?DeviceGeometry â™
+ /T The global temperature of the device denoted by $T$. â™
+ // temperature : Ω → ℠☠# T â™
+ temperature : QE Temperature ☠# T â™
+ /T The applied voltage at the bottom contact denoted by $U_1$. â™
+ voltage_bottom : QE ElectricPotential ☠# U_1 â™
+ /T The applied voltage at the top contact denoted by $U_2$. â™
+ voltage_top : QE ElectricPotential ☠# U_2 â™
- // prf : ⊦ k_B ⋅ T ≠0 . Energy
-
\ No newline at end of file
+ // prf : ⊦ k_B â‹… T ≠0 . Energy â™
+âš
\ No newline at end of file
diff --git a/source/mmt/poisson.mmt b/source/mmt/poisson.mmt
index 026c3b2..7f77a03 100644
--- a/source/mmt/poisson.mmt
+++ b/source/mmt/poisson.mmt
@@ -1,82 +1,82 @@
-namespace http://mathhub.info/MitM/Models/poisson
-import top http://mathhub.info/MitM/Models
-import qe http://mathhub.info/MMT/physics-units
+namespace http://mathhub.info/MitM/Models/poisson âš
+import top http://mathhub.info/MitM/Models âš
+import qe http://mathhub.info/MMT/physics-units âš
/T This is a theory containing the static dielectric permitivity constant
- of the semiconductor.
+ of the semiconductor. âš
theory PoissonParameters : top:?Base =
- /T The relative dielelectric permitivity constant denoted by $ε_r$.
- relative_dielectric_permittivity : real_lit # ε_r
- /T The static dielelectric permitivity constant denoted by $ε_s$.
- dielectric_permittivity : permittivity_dim = ε_r . ε_0 # ε_s
-
+ /T The relative dielelectric permitivity constant denoted by $ε_r$. â™
+ relative_dielectric_permittivity : real_lit ☠# ε_r ☠role Quantity â™
+ /T The static dielelectric permitivity constant denoted by $ε_s$. â™
+ dielectric_permittivity : permittivity_dim ☠= ε_r . ε_0 ☠# ε_s ☠role Quantity â™
+âš
/T This is a theory containing the total charge entering
- the right side of Poisson's equation.
+ the right side of Poisson's equation. âš
theory ChargeLaw : top:?Base =
- include device?DeviceGeometry
- include device?DopingProfile
- include ?PoissonParameters
- include top:/Species?ElectronsAndHoles
- include top:?SpatialChargeDensity
+ include device?DeviceGeometry â™
+ include device?DopingProfile â™
+ include ?PoissonParameters â™
+ include top:/Species?ElectronsAndHoles â™
+ include top:?SpatialChargeDensity â™
/T The total charge denoted by $Q$ composed of doping profile $C$ and
electron and hole densities $n$ and $p$, defined by
- $Q$ = $q$($C$+$p$ - $n$).
- total_charge_density : {x : Ω} ⊦ Q x ≠-q ⋅ ((C x) + (holes/z ⋅ (holes/density x)) + (electrons/z ⋅ (electrons/density x)))
-
+ $Q$ = $q$($C$+$p$ - $n$). â™
+ total_charge_density : {x : Ω} ⊦ Q x ≠-q â‹… ((C x) + (holes/z â‹… (holes/density x)) + (electrons/z â‹… (electrons/density x))) ☠role Law â™
+âš
// theory DisplacementLaw : top:?Base =
- include densities?ElectrostaticPotential
- include ?PoissonParameters
- include ?Displacement
+ include densities?ElectrostaticPotential â™
+ include ?PoissonParameters â™
+ include ?Displacement â™
- /T Expression for electric displacement denoted by $D$ = $- ε_s$ d/dx $ψ$
+ /T Expression for electric displacement denoted by $D$ = $- ε_s$ d/dx $ψ$ â™
- electric_displacement : Ω → displacement_dim
- = [x] -ε_s ⋅ (ψ ' x) # D
-
+ electric_displacement : Ω → displacement_dim â˜
+ = [x] -ε_s â‹… (ψ ' x) ☠# D â™
+âš
-/T This is a theory containing Poissons equation.
+/T This is a theory containing Poissons equation. âš
// theory PoissonEquation : top:?Base =
- include ?Charge
- include ?Displacement
+ include ?Charge â™
+ include ?Displacement â™
/T Defintion of the Poisson equation with total charge
- as right hand side.
- poisson_equation : ⊦ D ' ≠Q
+ as right hand side. â™
+ poisson_equation : ⊦ D ' ≠Qâ™
-
+âš
/T This is a theory containing build-in potential in
- thermodynamic equilibrium.
+ thermodynamic equilibrium. âš
// theory ThermodynamicEquilibrium : top:?Base =
- include ?Charge
+ include ?Charge â™
/T Value of build-in potential ψ_0 at top contact guranteeing
- local charge neutrality.
- equilibrium_potential_top : QE ElectricPotential # ψ_0_2
+ local charge neutrality. â™
+ equilibrium_potential_top : QE ElectricPotential ☠# ψ_0_2 â™
/T Value of build-in potential ψ_0 at bottom contact guranteeing
local charge neutrality.
- N.B. the build-in potential is given as U_b = $ψ_0_2 - ψ_0_1$ (Check!)
+ N.B. the build-in potential is given as U_b = $ψ_0_2 - ψ_0_1$ (Check!) â™
- equilibrium_potential_bottom : QE ElectricPotential # ψ_0_1
-
+ equilibrium_potential_bottom : QE ElectricPotential ☠# ψ_0_1 â™
+âš
-/T This is a theory containing the boundary values for the Poisson eqauation.
+/T This is a theory containing the boundary values for the Poisson eqauation. âš
// theory PoissonBoundaryConditions : top:?Base =
- include ?ThermodynamicEquilibrium
+ include ?ThermodynamicEquilibrium â™
/T Boundary value for electrostatic potential at top contact
- for an applied voltage $U_1$.
- potential_top : QE ElectricPotential = ψ_0_1 + U_1 # ψ_1
+ for an applied voltage $U_1$. â™
+ potential_top : QE ElectricPotential ☠= ψ_0_1 + U_1 ☠# ψ_1 â™
/T Boundary value for electrostatic potential at bottom contact
for an applied voltage $U_2$.
- N.B.: the applied bias voltage is U_bias = $U_2-U_1$
- potential_bottom : QE ElectricPotential = ψ_0_2 + U_2 # ψ_2
-
\ No newline at end of file
+ N.B.: the applied bias voltage is U_bias = $U_2-U_1$ â™
+ potential_bottom : QE ElectricPotential ☠= ψ_0_2 + U_2 ☠# ψ_2 â™
+âš
\ No newline at end of file
diff --git a/source/mmt/recombination.mmt b/source/mmt/recombination.mmt
index 50e33d3..eff374d 100644
--- a/source/mmt/recombination.mmt
+++ b/source/mmt/recombination.mmt
@@ -1,27 +1,27 @@
-namespace http://mathhub.info/MitM/Models/recombination
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/recombination âš
+import top http://mathhub.info/MitM/Models âš
/T This is a theory containing the general structure for
- a recombination rate.
+ a recombination rate. âš
theory Recombination : top:?Base =
- include top:/Species?ElectronsAndHoles
- include top:?RecombinationCoefficient
- include top:?RecombinationRate
- /T Recombination rate for right hand side of continuity equations.
+ include top:/Species?ElectronsAndHoles â™
+ include top:?RecombinationCoefficient â™
+ include top:?RecombinationRate â™
+ /T Recombination rate for right hand side of continuity equations. â™
recombination_rate : {x : Ω} ⊦ R x â‰
(r (electrons/spatialdensity x) (holes/spatialdensity x)) â‹… (electrons/spatialdensity x) â‹… (holes/spatialdensity x)
- â‹… (1 - (exponential (q â‹… ((electrons/fermi/potential x) - (holes/fermi/potential x)) / (k_B â‹… T))))
-
+ â‹… (1 - (exponential (q â‹… ((electrons/fermi/potential x) - (holes/fermi/potential x)) / (k_B â‹… T)))) â™
+âš
-/T Kernel for spontaneous recombination with coefficient B.
+/T Kernel for spontaneous recombination with coefficient B. âš
theory SpontaneousRecombination : top:?Base =
- include ?Recombination
+ include ?Recombination â™
- /T The coefficient for the sponanteous recombination rate is denoted by $B$
- spontaneous_recombination_coefficient : QE (Volume /' SItime) # B
- /T Formula for sponanteous recombination $r$($n$,$p$) = $B$
- axiom_spontaneous : {x,y} ⊦ r x y ≠B role Simplify
-
+ /T The coefficient for the sponanteous recombination rate is denoted by $B$ â™
+ spontaneous_recombination_coefficient : QE (Volume /' SItime) ☠# Bâ™
+ /T Formula for sponanteous recombination $r$($n$,$p$) = $B$ â™
+ axiom_spontaneous : {x,y} ⊦ r x y ≠B ☠role Simplify â™
+âš
diff --git a/source/mmt/species.mmt b/source/mmt/species.mmt
index 8488f61..8fd488f 100644
--- a/source/mmt/species.mmt
+++ b/source/mmt/species.mmt
@@ -1,21 +1,21 @@
-namespace http://mathhub.info/MitM/Models/Species
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/Species âš
+import top http://mathhub.info/MitM/Models âš
theory Species : top:?Base =
- include densities?DensityLaw
- include top:?SpatialCurrentDensity
- // include CurrentLaw
-
+ include densities?DensityLaw â™
+ include top:?SpatialCurrentDensity â™
+ // include CurrentLaw â™
+âš
theory Electrons : top:?Base =
- structure electrons : ?Species =
-
+ structure electrons : ?Species = âš
+âš
theory Holes : top:?Base =
- structure holes : ?Species =
-
+ structure holes : ?Species = âš
+âš
theory ElectronsAndHoles : top:?Base =
- include ?Electrons
- include ?Holes
-
\ No newline at end of file
+ include ?Electrons â™
+ include ?Holes â™
+âš
\ No newline at end of file
diff --git a/source/thermistor/quantities.mmt b/source/thermistor/quantities.mmt
index e9a9c5d..9010f75 100644
--- a/source/thermistor/quantities.mmt
+++ b/source/thermistor/quantities.mmt
@@ -1,229 +1,229 @@
-namespace http://mathhub.info/MitM/Models/thermistor
-import qe http://mathhub.info/MMT/physics-units
-import top http://mathhub.info/MitM/Models
+namespace http://mathhub.info/MitM/Models/thermistor âš
+import qe http://mathhub.info/MMT/physics-units âš
+import top http://mathhub.info/MitM/Models âš
-/T This theory intentionally left empty. It has a narrative in sTeX
-/T Background
-theory Device =
+/T This theory intentionally left empty. It has a narrative in sTeX âš
+/T Background âš
+theory Device = âš
-/T This is a theory containing description of device geometry.
-/T Parameter
+/T This is a theory containing description of device geometry. âš
+/T Parameter âš
theory DeviceGeometry : top:?Base =
- include ?Device
- // domain_prop : â„3 → bool
- domain_prop : ℠→ bool
- /T The one-dimensional spatial domain of the device (denoted by $Ω$).
- domain : type = pred domain_prop # Ω
-
+ include ?Device â™
+ // domain_prop : â„3 → bool â™
+ domain_prop : ℠→ bool â™
+ /T The one-dimensional spatial domain of the device (denoted by $Ω$). â™
+ domain : type ☠= pred domain_prop ☠# Ω â™
+âš
theory SpatialPotential : top:?Base =
- include ?DeviceGeometry
+ include ?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- potential : Ω → (QE ElectricPotential) # φ
-
+ usually denoted by $φ$. â™
+ potential : Ω → (QE ElectricPotential) ☠# φâ™
+âš
theory ElectricFieldStrength : qe:?QEBase =
- electricfieldstrength_dim : type = QE (ElectricPotential /' SIlength)
- electricfieldstrength : electricfieldstrength_dim
-
+ electricfieldstrength_dim : type ☠= QE (ElectricPotential /' SIlength) â™
+ electricfieldstrength : electricfieldstrength_dim â™
+âš
theory SpatialElectricField : top:?Base =
- include ?DeviceGeometry
- include ?ElectricFieldStrength
+ include ?DeviceGeometry â™
+ include ?ElectricFieldStrength â™
/T Spatial variation of the electric field strength,
- usually denoted by $E$.
- electricfield : Ω → (electricfieldstrength_dim) # E
-
+ usually denoted by $E$. â™
+ electricfield : Ω → (electricfieldstrength_dim) ☠# Eâ™
+âš
theory CurrentDensity : qe:?QEBase =
- // meta modeltype physical_quantity
- currentdensity_dim : type = QE (SIcurrent /' Area)
- currentdensity : currentdensity_dim
-
+ // meta modeltype physical_quantity â™
+ currentdensity_dim : type ☠= QE (SIcurrent /' Area) â™
+ currentdensity : currentdensity_dim â™
+âš
theory SpatialCurrentDensity : top:?Base =
- include ?DeviceGeometry
- include ?CurrentDensity
- currentdensity : Ω → (currentdensity_dim) # j 1
-
+ include ?DeviceGeometry â™
+ include ?CurrentDensity â™
+ currentdensity : Ω → (currentdensity_dim) ☠# j 1 â™
+âš
theory ElectricalConductivity : qe:?QEBase =
- // meta modeltype physical_quantity
- electricalconductitvity_dim : type = QE (SIcurrent /' (ElectricPotential * SIlength))
- electricalconductitvity : electricalconductitvity_dim
-
+ // meta modeltype physical_quantity â™
+ electricalconductitvity_dim : type ☠= QE (SIcurrent /' (ElectricPotential * SIlength)) â™
+ electricalconductitvity : electricalconductitvity_dim â™
+âš
theory SpatialElectricalConductivity : top:?Base =
- include ?DeviceGeometry
- include ?ElectricalConductivity
- spatialelectricalconductivity : Ω → (electricalconductitvity_dim) # σ 1
-
+ include ?DeviceGeometry â™
+ include ?ElectricalConductivity â™
+ spatialelectricalconductivity : Ω → (electricalconductitvity_dim) ☠# σ 1 â™
+âš
theory SpatialReferenceConductivity : top:?Base =
- include ?DeviceGeometry
- include ?ElectricalConductivity
- spatialreferenceconductivity : Ω → (electricalconductitvity_dim) # σ_0 1
-
+ include ?DeviceGeometry â™
+ include ?ElectricalConductivity â™
+ spatialreferenceconductivity : Ω → (electricalconductitvity_dim) ☠# σ_0 1 â™
+âš
theory SpatialReferenceElectricalField : top:?Base =
- include ?DeviceGeometry
- include ?ElectricalFieldStrength
- referebceelectricfield : Ω → (electricfieldstrength_dim) # Eref
-
+ include ?DeviceGeometry â™
+ include ?ElectricalFieldStrength â™
+ referebceelectricfield : Ω → (electricfieldstrength_dim) ☠# Erefâ™
+âš
theory SpatialFieldEnhancement : top:?Base =
- include ?DeviceGeometry
- spatialfieldenhancement : Ω → ℠# G
-
+ include ?DeviceGeometry â™
+ spatialfieldenhancement : Ω → ℠☠# Gâ™
+âš
theory SpatialLaplacep : top:?Base =
- include ?DeviceGeometry
- spatiallaplacep : Ω → ℠# p
-
+ include ?DeviceGeometry â™
+ spatiallaplacep : Ω → ℠☠# pâ™
+âš
theory SpatialArrheniusFaktor : top:?Base =
- include ?DeviceGeometry
- spatialarrheniusfaktor : Ω → ℠# F
-
+ include ?DeviceGeometry â™
+ spatialarrheniusfaktor : Ω → ℠☠# Fâ™
+âš
theory Heat : qe:?QEBase =
- // meta modeltype physical_quantity
- heat_dim : type = QE (Energy)
- heat : heat_dim
-
+ // meta modeltype physical_quantity â™
+ heat_dim : type ☠= QE (Energy) â™
+ heat : heat_dim â™
+âš
theory SpatialHeatSource : top:?Base =
- include ?DeviceGeometry
- include ?Heat
- spatialheatsource : Ω → (heat_dim) # Q 1
-
+ include ?DeviceGeometry â™
+ include ?Heat â™
+ spatialheatsource : Ω → (heat_dim) ☠# Q 1 â™
+âš
theory SpatialJouleHeat : top:?Base =
- include ?DeviceGeometry
- include ?Heat
- spatialheatsource : Ω → (heat_dim) # Q_Joule 1
-
+ include ?DeviceGeometry â™
+ include ?Heat â™
+ spatialheatsource : Ω → (heat_dim) ☠# Q_Joule 1 â™
+âš
theory ThermalConductivity : qe:?QEBase =
- include ?Heat
- // meta modeltype physical_quantity
- thermalconductitvity_dim : type = QE ( Energy /' (SIlength * SItemperature))
- thermalconductitvity : thermalconductitvity_dim
-
+ include ?Heat â™
+ // meta modeltype physical_quantity â™
+ thermalconductitvity_dim : type ☠= QE ( Energy /' (SIlength * SItemperature)) â™
+ thermalconductitvity : thermalconductitvity_dim â™
+âš
theory SpatialThermalConductivity : top:?Base =
- include ?DeviceGeometry
- include ?ThermalConductivity
- spatialthermalconductivity : Ω → (thermalconductitvity_dim) # λ 1
-
+ include ?DeviceGeometry â™
+ include ?ThermalConductivity â™
+ spatialthermalconductivity : Ω → (thermalconductitvity_dim) ☠# λ 1 â™
+âš
theory ThermalHeatFlux : qe:?QEBase =
- // meta modeltype physical_quantity electricfield_law : {x : Ω} ⊦ E x ≠- ((φ ') x) / unitlengt
- thermalheatflux_dim : type = QE (Energy /' Area)
- thermalheatflux : thermalheatflux_dim
-
+ // meta modeltype physical_quantity electricfield_law : {x : Ω} ⊦ E x ≠- ((φ ') x) / unitlengt â™
+ thermalheatflux_dim : type ☠= QE (Energy /' Area) â™
+ thermalheatflux : thermalheatflux_dim â™
+âš
theory SpatialHeatFluxDensity : top:?Base =
- include ?DeviceGeometry
- include ?ThermalHeatFlux
- heatfluxdensity : Ω → (thermalheatflux_dim) # q 1
-
+ include ?DeviceGeometry â™
+ include ?ThermalHeatFlux â™
+ heatfluxdensity : Ω → (thermalheatflux_dim) ☠# q 1 â™
+âš
theory SpatialTemperature : top:?Base =
- include ?DeviceGeometry
+ include ?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- potential : Ω → (QE SItemperature) # T
-
+ usually denoted by $φ$. â™
+ potential : Ω → (QE SItemperature) ☠# Tâ™
+âš
theory ReferenceTemperature : top:?Base =
-include ?DeviceGeometry
+include ?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- referencetemperature : QE SItemperature # Tref
-
+ usually denoted by $φ$. â™
+ referencetemperature : QE SItemperature ☠# Trefâ™
+âš
theory ActivationEnergy : top:?Base =
-include ?DeviceGeometry
+include ?DeviceGeometry â™
/T Spatial variation of the potential,
- usually denoted by $φ$.
- activationenergy : QE Energy # E_act
-
+ usually denoted by $φ$. â™
+ activationenergy : QE Energy ☠# E_actâ™
+âš
theory ElectricFieldLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialElectricField
- include ?SpatialPotential
- electricfield_law : {x : Ω} ⊦ E x ≠-((QEderiv φ) x)
-
+ include ?DeviceGeometry â™
+ include ?SpatialElectricField â™
+ include ?SpatialPotential â™
+ electricfield_law : {x : Ω} ⊦ E x ≠-((QEderiv φ) x) â™
+âš
theory OhmsLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialCurrentDensity
- include ?SpatialElectricField
- include ?SpatialElectricalConductivity
- ohmscurrent_law : {x : Ω} ⊦ j ≠(σ x) ⋅ (E x)
-
+ include ?DeviceGeometry â™
+ include ?SpatialCurrentDensity â™
+ include ?SpatialElectricField â™
+ include ?SpatialElectricalConductivity â™
+ ohmscurrent_law : {x : Ω} ⊦ j ≠(σ x) â‹… (E x) â™
+âš
theory KirchhoffsCurrentLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialCurrentDensity
- kirchhoffscurrent_law : {x : Ω} ⊦ ((QEderiv j) x) ≠0
-
+ include ?DeviceGeometry â™
+ include ?SpatialCurrentDensity â™
+ kirchhoffscurrent_law : {x : Ω} ⊦ ((QEderiv j) x) ≠0â™
+âš
theory JouleHeat : top:?Base =
- include ?DeviceGeometry
- include ?SpatialJouleHeat
- include ?SpatialCurrentDensity
- include ?SpatialElectricField
- jouleheat : {x : Ω} ⊦ Q_Joule ≠(j x) ⋅ (E x)
-
+ include ?DeviceGeometry â™
+ include ?SpatialJouleHeat â™
+ include ?SpatialCurrentDensity â™
+ include ?SpatialElectricField â™
+ jouleheat : {x : Ω} ⊦ Q_Joule ≠(j x) â‹… (E x) â™
+âš
theory FieldEnhancement : top:?Base =
- include ?DeviceGeometry
- include ?SpatialFieldEnhancement
- include ?SpatialElectricField
- include ?SpatialReferenceElectricField
- include ?SpatialLaplacep
+ include ?DeviceGeometry â™
+ include ?SpatialFieldEnhancement â™
+ include ?SpatialElectricField â™
+ include ?SpatialReferenceElectricField â™
+ include ?SpatialLaplacep â™
- fieldenhancement : {x : Ω} ⊦ G ≠|(E x) / (Eref x)|^(p-2)
-
+ fieldenhancement : {x : Ω} ⊦ G ≠|(E x) / (Eref x)|^(p-2) â™
+âš
theory ArrheniusLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialArrheniusFactor
- include ?SpatialActivationEnergy
- include ?ReferenceTemperature
- include ?SpatialTemperature
+ include ?DeviceGeometry â™
+ include ?SpatialArrheniusFactor â™
+ include ?SpatialActivationEnergy â™
+ include ?ReferenceTemperature â™
+ include ?SpatialTemperature â™
- arrhenius_law : {x : Ω} ⊦ F ≠exp( ( E_act / k_B) ⋅ (1 / (T x) - 1 / Tref)
-
+ arrhenius_law : {x : Ω} ⊦ F ≠exp( ( E_act / k_B) â‹… (1 / (T x) - 1 / Tref) â™
+âš
theory ConductivityLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialElectricalConductivity
- include ?SpatialReferenceConductivity
- include ?SpatialArrheniusFactor
- include ?SpatialFieldEnhancement
- include ?ReferenceTemperature
- include ?SpatialTemperature
+ include ?DeviceGeometry â™
+ include ?SpatialElectricalConductivity â™
+ include ?SpatialReferenceConductivity â™
+ include ?SpatialArrheniusFactor â™
+ include ?SpatialFieldEnhancement â™
+ include ?ReferenceTemperature â™
+ include ?SpatialTemperature â™
- conductivity_law : {x : Ω} ⊦ σ ≠(σ_0 x) ⋅ (F x) ⋅ G(x)
-
+ conductivity_law : {x : Ω} ⊦ σ ≠(σ_0 x) â‹… (F x) â‹… G(x) â™
+âš
theory FouriersLaw : top:?Base =
- include ?DeviceGeometry
- include ?SpatialThermalConductivity
- include ?SpatialTemperature
+ include ?DeviceGeometry â™
+ include ?SpatialThermalConductivity â™
+ include ?SpatialTemperature â™
- conductivity_law : {x : Ω} ⊦ σ ≠(σ_0 x) ⋅ (F x) ⋅ (G x)
-
+ conductivity_law : {x : Ω} ⊦ σ ≠(σ_0 x) â‹… (F x) â‹… (G x) â™
+âš
\ No newline at end of file
--
GitLab